let n be Nat; :: thesis: for x, y being Element of REAL n holds |.(x + y).| <= |.x.| + |.y.|
let x, y be Element of REAL n; :: thesis: |.(x + y).| <= |.x.| + |.y.|
( len x = n & len y = n ) by FINSEQ_1:def 18;
hence |.(x + y).| <= |.x.| + |.y.| by EUCLID_2:38; :: thesis: verum