`BookProof.ClosureUniqueness.clDom_eq_of_clGraph_eq` {T₁ : D₁ →ₗ[ℂ] F} {T₂ : D₂ →ₗ[ℂ] F} (h : clGraph T₁ = clGraph T₂) : clDom T₁ = clDom T₂

Initializing...

`BookProof.ClosureUniqueness.clDom_eq_of_clGraph_eq` {T₁ : D₁ →ₗ[ℂ] F} {T₂ : D₂ →ₗ[ℂ] F} (h : clGraph T₁ = clGraph T₂) : clDom T₁ = clDom T₂ · Prove2Me