---

Step * of Lemma rv-orthog-ext_wf

∀rv:InnerProductSpace. ∀f:Point ⟶ Point.
  rv-orthog-ext(rv;f) ∈ ∀x,y:Point.  (f x # f y ⇒ x # y) supposing Orthogonal(f)
BY
{ (Auto
   THEN (Assert TERMOF{rv-orthogonal-implies-extensional-ext:o, 1:l, i:l} rv f ∈ ∀x,y:Point.  (f x # f y ⇒ x # y) BY
               Auto)
   ) }

1
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. Orthogonal(f)
4. TERMOF{rv-orthogonal-implies-extensional-ext:o, 1:l, i:l} rv f ∈ ∀x,y:Point.  (f x # f y ⇒ x # y)
⊢ rv-orthog-ext(rv;f) ∈ ∀x,y:Point.  (f x # f y ⇒ x # y)

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}f:Point  {}\mrightarrow{}  Point.
    rv-orthog-ext(rv;f)  \mmember{}  \mforall{}x,y:Point.    (f  x  \#  f  y  {}\mRightarrow{}  x  \#  y)  supposing  Orthogonal(f)


By

---

Latex:
(Auto
  THEN  (Assert  TERMOF\{rv-orthogonal-implies-extensional-ext:o,  1:l,  i:l\}  rv  f  \mmember{}  \mforall{}x,y:Point.
                                                                                                                                                                  (f  x  \#  f  y
                                                                                                                                                                  {}\mRightarrow{}  x  \#  y)  BY
                          Auto)
  )

---

Home Index