---

Step * of Lemma real-matrix-add_functionality

∀[a,b:ℕ]. ∀[A1,A2,B1,B2:ℝ(a × b)].  (A1 + B1 ≡ A2 + B2) supposing (A1 ≡ A2 and B1 ≡ B2)
BY
{ (Auto
   THEN All (RepUR ``rmatrix reqmatrix real-matrix-add``)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN RWO "-4 -3" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbN{}].  \mforall{}[A1,A2,B1,B2:\mBbbR{}(a  \mtimes{}  b)].    (A1  +  B1  \mequiv{}  A2  +  B2)  supposing  (A1  \mequiv{}  A2  and  B1  \mequiv{}  B2)


By

---

Latex:
(Auto
  THEN  All  (RepUR  ``rmatrix  reqmatrix  real-matrix-add``)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RWO  "-4  -3"  0
  THEN  Auto)

---

Home Index