---

Step * of Lemma real-matrix-times_functionality

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

---

Latex:

---

Latex:
\mforall{}[n,a,b:\mBbbN{}].  \mforall{}[A1,A2:\mBbbR{}(a  \mtimes{}  n)].  \mforall{}[B1,B2:\mBbbR{}(n  \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-times``)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RWO  "-4  -3"  0
  THEN  Auto)

---

Home Index