---

Step * of Lemma rv-mul-mul

∀[rv:RealVectorSpace]. ∀[a,b:ℝ]. ∀[x:Point].  a*b*x ≡ a * b*x
BY
{ (Auto
   THEN (D 1 THENA Auto)
   THEN Unfolds ``rv-mul rv-add`` 0
   THEN OnMaybeHyp 10 (\h. (MemTypeHD h
                            THEN ∀h:hyp. Fold `member` h 
                            THEN Try (MemCD)
                            THEN (Unhide THENM (ExRepD THEN BackThruSomeHyp))
                            THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[rv:RealVectorSpace].  \mforall{}[a,b:\mBbbR{}].  \mforall{}[x:Point].    a*b*x  \mequiv{}  a  *  b*x


By

---

Latex:
(Auto
  THEN  (D  1  THENA  Auto)
  THEN  Unfolds  ``rv-mul  rv-add``  0
  THEN  OnMaybeHyp  10  (\mbackslash{}h.  (MemTypeHD  h
                                                    THEN  \mforall{}h:hyp.  Fold  `member`  h 
                                                    THEN  Try  (MemCD)
                                                    THEN  (Unhide  THENM  (ExRepD  THEN  BackThruSomeHyp))
                                                    THEN  Auto)))

---

Home Index