---

Step * of Lemma rcp_functionality

∀[a1,b1,a2,b2:ℝ^3].  (req-vec(3;(a1 x b1);(a2 x b2))) supposing (req-vec(3;b1;b2) and req-vec(3;a1;a2))
BY
{ (Unfolds ``real-vec req-vec rcp`` 0 THEN Auto THEN IntSegCases (-1) THEN Reduce 0 THEN RWW "5 6" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a1,b1,a2,b2:\mBbbR{}\^{}3].
    (req-vec(3;(a1  x  b1);(a2  x  b2)))  supposing  (req-vec(3;b1;b2)  and  req-vec(3;a1;a2))


By

---

Latex:
(Unfolds  ``real-vec  req-vec  rcp``  0
  THEN  Auto
  THEN  IntSegCases  (-1)
  THEN  Reduce  0
  THEN  RWW  "5  6"  0
  THEN  Auto)

---

Home Index