---

Step * of Lemma transpose-identity-matrix

∀[r:RngSig]. ∀[n:ℕ].  (I' = I ∈ Matrix(n;n;r))
BY
{ ((Auto THEN RepUR ``matrix-transpose identity-matrix`` 0) THEN EqCDA THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[r:RngSig].  \mforall{}[n:\mBbbN{}].    (I'  =  I)


By

---

Latex:
((Auto  THEN  RepUR  ``matrix-transpose  identity-matrix``  0)  THEN  EqCDA  THEN  AutoSplit)

---

Home Index