A⋄ がスカラー倍で閉じていることは、 任意の f∈A∗ とスカラー k∈󱀊∖{0} に対して Kerf=Kerkf であることからすぐに分かる。 以下、 A⋄ が和で閉じていることを示す。

任意に元 f,g∈A⋄ をとると、 A の余有限イデアル I⊆Kerf および J⊆Kerg がとれる。 ここで、 p:A/(I∩J)→A/I を自然に定まる写像とすると、 これは明らかに全射であるから Imp=A/I が分かる。 また、 Kerp≅I/(I∩J)≅(I+J)/J も成り立つ。 したがって、 I と J は余有限であるから、 dimA/(I∩J) = dimKerp+dimImp = dim(I+J)/J+dimA/I ≤ dimA/J+dimA/I < ∞ が分かり、 これより I∩J も余有限である。 I∩J⊆Ker(f+g) であるから、 これより f+g∈A⋄ が得られた。 以上で、 A⋄ は和に関して閉じている。

任意に元 h∈(A⊗B)⋄ をとると、 A⊗B の余有限イデアル K⊆Kerh がとれる。 これに対し、 I := {a∈A∣a⊗1∈K} J := {b∈B∣1⊗b∈K} とおくと、 まずこれらはどちらもイデアルである。 ここで、 s: A ⟶ A⊗B a ⟼ a⊗1 p: A⊗B ⟶ (A⊗B)/K a⊗b ⟼ [a⊗b] とおくと、 I=s−1(K)=Ker(p∘s) であるから、 準同型定理によって A/I≅Im(p∘s)⊆(A⊗B)/K が成り立つ。 K は余有限であったので、 (A⊗B)/K は有限次元であり、 その部分空間となる A/I も有限次元であり、 したがって I は余有限である。 同様の議論により、 J も余有限であることが分かる。

さて、 q:A⊗B↠A/I⊗B/J を商空間への射影のテンソル積とすると、 I と J の定義によって、 A⊗B󱀊A/I⊗B/Jhqh󰎘 を可換にする線型写像 h󰎘 が存在する。 これは元 h󰎘∈(A/I⊗B/J)∗ が定めるが、 今 A/I と B/J は有限次元であることが分かっているので、 (A/I⊗B/J)∗≅(A/I)∗⊗(B/J)∗ が成り立ち、 h󰎘∈(A/I)∗⊗(B/J)∗ と見なせる。 そこで、 fi󰎘∈(A/I)∗ と gi󰎘∈(B/J)∗ たちによって、 h󰎘=:󰄚i(fi󰎘⊗gi󰎘) と表す。

r:A↠A/I を射影として fi:=fi󰎘∘r とおくと、 fi∈A∗ が定まる。 明らかに I⊆Kerfi であって、 I は余有限だったので、 fi∈A⋄ が成り立つ。 同様にして gi∈B⋄ も定めると、 h=󰄚i(fi⊗gi) と書ける。 したがって、 h∈A⋄⊗B⋄ が成り立つ。 以上により、 A⋄⊗B⋄⊇(A⊗B)⋄ が示された。

逆に任意に f∈A⋄ と g∈B⋄ をとる。 このとき、 余有限イデアル I⊆Kerf と J⊆Kerg がとれる。 すると、 K:=A⊗J+I⊗B⊆Ker(f⊗g) が分かる。 この K はまず明らかにイデアルである。 さらに、 上と同じ q:A⊗B↠A/I⊗B/J をとれば、 準同型定理によって (A⊗B)/K≅Imq⊆A/I⊗B/J が成り立つが、 この右辺は有限次元なので、 (A⊗B)/K も有限次元で、 K は余有限である。 したがって、 f⊗g∈(A⊗B)⋄ が成り立つ。 以上により、 A⋄⊗B⋄⊆(A⊗B)⋄ も示された。

任意に元 f∈A⋄ をとる。 すると、 定義によってある A の余有限イデアル I⊆Kerf が存在する。 任意の a∈A および u∈I に対し、 I⊆Kerf によって、 μ∗(f)(a⊗u)=f(μ(a⊗u))=f(au)=0 であるから、 A⊗I⊆Kerμ∗(f) が成り立つ。 同様の計算により I⊗A⊆Kerμ∗(f) も成り立つ。 したがって、 K:=A⊗I+I⊗A とおけば K⊆Kerμ∗(f) が成り立つ。 補題 1.8 の証明で行った議論と同様にして、 K は余有限イデアルであることが分かるので、 μ∗(f)∈(A⊗A)⋄ が得られる。 以上により、 補題 1.8 を用いて μ∗(A⋄)⊆(A⊗A)⋄=A⋄⊗A⋄ が示された。

定義に従えば、 容易に確かめられる。

作用 C∗↷C∗∗ を、 ·: C∗×C∗∗ ⟶ C∗∗ (f,v) ⟼ ❲ C∗ ⟶ 󱀊 f󰎘 ⟼ v(f󰎘f)❲ で定める。 なお、 f󰎘f とは、 C∗ の代数としての f󰎘 と f の積である。

任意に c∈C と f∈C∗ をとる。 すると、 各 f󰎘∈C∗ に対し、 (f·i(c))(f󰎘) = i(c)(f󰎘f) = (f󰎘f)c = 󰄚cf󰎘(c(1))f(c(2)) が成り立つ。 したがって、 f·i(c)=󰄚ci(c(1))f(c(2)) と書ける。 したがって、 c∈C を固定すると、 C∗·i(c) は i(c(1)) たちで張られる線型空間に含まれるので、 C∗·i(c) は有限次元である。

V:=C∗·i(c)⊆C∗∗ とおき、 I:={f∈C∗∣f·V=0} と定めると、 これはイデアルである。 さらに、 s: C∗ ⟶ End(V) f ⟼ ❲ V ⟶ V v ⟼ f·v❲ とおくと、 I≅Kers と書ける。 したがって、 C∗/I≅Ims⊆End(V) であり、 V が有限次元であることから End(V) も有限次元なので、 C∗/I も有限次元で、 I は余有限である。

ここで、 任意の u∈I に対し、 i(c)∈V であるから、 i(c)(u)=(u·i(c))(1)=0 が成り立つ。 したがって、 I⊆Keri(c) であって I は余有限だったので、 i(c)∈C∗⋄ が成り立つ。

余代数 C に対して、 補題 1.11 によって i:C→C∗∗ の終域を狭めたものを ψ:C→C∗⋄ とおく。 また、 代数 A に対しては、 j:A⋄↪A∗ を包含写像として、 合成 AA∗∗A⋄∗ij∗ を φ:A→A⋄∗ とおく。 すると、 示したい全単射は、 HomAlg(A,C∗) ⟶ HomCoalg(C,A⋄) s ⟼ s⋄∘ψ t∗∘φ ⟻ t で与えられる。