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 CARD_1:def 7;
p + q = p + q by EUCLID:64;
hence |.(p + q).| <= |.p.| + |.q.| by A1, Th38; :: thesis: verum