---

Step * 1 1 of Lemma rv-orthog-ext_wf

.....equality..... 
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)
⊢ TERMOF{rv-orthogonal-implies-extensional-ext:o, 1:l, i:l} rv f ~ rv-orthog-ext(rv;f)
BY
{ (RW (SubC (TagC (mk_tag_term 3))) 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  rv  :  InnerProductSpace
2.  f  :  Point  {}\mrightarrow{}  Point
3.  Orthogonal(f)
4.  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)
\mvdash{}  TERMOF\{rv-orthogonal-implies-extensional-ext:o,  1:l,  i:l\}  rv  f  \msim{}  rv-orthog-ext(rv;f)


By

---

Latex:
(RW  (SubC  (TagC  (mk\_tag\_term  3)))  0  THEN  Auto)

---

Home Index