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