---

Step * of Lemma hyptrans_functionality

∀[rv:InnerProductSpace]. ∀[e1,x1:Point]. ∀[t1:ℝ]. ∀[e2,x2:Point]. ∀[t2:ℝ].
  (hyptrans(rv;e1;t1;x1) ≡ hyptrans(rv;e2;t2;x2)) supposing (x1 ≡ x2 and e1 ≡ e2 and (t1 = t2))
BY
{ (Auto THEN Unfold `hyptrans` 0 THEN RWO "-1 -2 -3" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[e1,x1:Point].  \mforall{}[t1:\mBbbR{}].  \mforall{}[e2,x2:Point].  \mforall{}[t2:\mBbbR{}].
    (hyptrans(rv;e1;t1;x1)  \mequiv{}  hyptrans(rv;e2;t2;x2))  supposing  (x1  \mequiv{}  x2  and  e1  \mequiv{}  e2  and  (t1  =  t2))


By

---

Latex:
(Auto  THEN  Unfold  `hyptrans`  0  THEN  RWO  "-1  -2  -3"  0  THEN  Auto)

---

Home Index