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