---

Step * of Lemma rv-congruent_functionality

∀n:ℕ. ∀a1,a2,b1,b2,c1,c2,d1,d2:ℝ^n.
  (req-vec(n;a1;a2) ⇒ req-vec(n;b1;b2) ⇒ req-vec(n;c1;c2) ⇒ req-vec(n;d1;d2) ⇒ (a1b1=c1d1 ⇐⇒ a2b2=c2d2))
BY
{ (Auto THEN ParallelLast THEN ((RWO "-5 -4 -3 -2" (-1) THEN Auto) ORELSE (RWO "-5< -4< -3< -2<" (-1) THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a1,a2,b1,b2,c1,c2,d1,d2:\mBbbR{}\^{}n.
    (req-vec(n;a1;a2)
    {}\mRightarrow{}  req-vec(n;b1;b2)
    {}\mRightarrow{}  req-vec(n;c1;c2)
    {}\mRightarrow{}  req-vec(n;d1;d2)
    {}\mRightarrow{}  (a1b1=c1d1  \mLeftarrow{}{}\mRightarrow{}  a2b2=c2d2))


By

---

Latex:
(Auto
  THEN  ParallelLast
  THEN  ((RWO  "-5  -4  -3  -2"  (-1)  THEN  Auto)  ORELSE  (RWO  "-5<  -4<  -3<  -2<"  (-1)  THEN  Auto)))

---

Home Index