---

Step * of Lemma real-matrix-scalar-mul_functionality

∀[a,b:ℕ]. ∀[c1,c2:ℝ]. ∀[A,B:ℝ(a × b)].  (c1*A ≡ c2*B) supposing ((c1 = c2) and A ≡ B)
BY
{ (Auto
   THEN All (RepUR ``rmatrix reqmatrix real-matrix-scalar-mul``)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN RWO "-4 -3" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbN{}].  \mforall{}[c1,c2:\mBbbR{}].  \mforall{}[A,B:\mBbbR{}(a  \mtimes{}  b)].    (c1*A  \mequiv{}  c2*B)  supposing  ((c1  =  c2)  and  A  \mequiv{}  B)


By

---

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

---

Home Index