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;
thus |.(p + q).| <= |.p.| + |.q.| by A1, Th15; :: thesis: verum