let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds
( p,p are_orthogonal iff p = 0. (TOP-REAL n) )
let p be Point of (TOP-REAL n); :: thesis: ( p,p are_orthogonal iff p = 0. (TOP-REAL n) )
( p,p are_orthogonal iff |(p,p)| = 0 ) by RVSUM_1:def 17;
hence ( p,p are_orthogonal iff p = 0. (TOP-REAL n) ) by Th63; :: thesis: verum