let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n) holds abs |(p,q)| <= |.p.| * |.q.|
let p, q be Point of (TOP-REAL n); :: thesis: abs |(p,q)| <= |.p.| * |.q.|
( len p = n & len q = n ) by FINSEQ_1:def 18;
hence abs |(p,q)| <= |.p.| * |.q.| by Th37; :: thesis: verum