let x, y be Real; :: thesis: for v being Element of (REAL-NS 2) st v = <*x,y*> holds

||.v.|| <= |.x.| + |.y.|

let v be Element of (REAL-NS 2); :: thesis: ( v = <*x,y*> implies ||.v.|| <= |.x.| + |.y.| )

reconsider z = x + (y * <i>) as Complex ;

assume v = <*x,y*> ; :: thesis: ||.v.|| <= |.x.| + |.y.|

then |.z.| = ||.v.|| by Lm14;

hence ||.v.|| <= |.x.| + |.y.| by Lm15; :: thesis: verum

||.v.|| <= |.x.| + |.y.|

let v be Element of (REAL-NS 2); :: thesis: ( v = <*x,y*> implies ||.v.|| <= |.x.| + |.y.| )

reconsider z = x + (y * <i>) as Complex ;

assume v = <*x,y*> ; :: thesis: ||.v.|| <= |.x.| + |.y.|

then |.z.| = ||.v.|| by Lm14;

hence ||.v.|| <= |.x.| + |.y.| by Lm15; :: thesis: verum