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