let x, y be Real; :: thesis: for v being Element of (REAL-NS 2) st v = <*x,y*> holds
||.v.|| <= (abs x) + (abs y)
let v be Element of (REAL-NS 2); :: thesis: ( v = <*x,y*> implies ||.v.|| <= (abs x) + (abs y) )
assume A1: v = <*x,y*> ; :: thesis: ||.v.|| <= (abs x) + (abs y)
reconsider z = x + (y * <i> ) as Complex by XCMPLX_0:def 2;
|.z.| = ||.v.|| by A1, Lm034;
hence ||.v.|| <= (abs x) + (abs y) by Lm035; :: thesis: verum