let x, y be Real; :: thesis: for z being Complex
for v being Element of (REAL-NS 2) st z = x + (y * <i> ) & v = <*x,y*> holds
|.z.| = ||.v.||
let z be Complex; :: thesis: for v being Element of (REAL-NS 2) st z = x + (y * <i> ) & v = <*x,y*> holds
|.z.| = ||.v.||
let v be Element of (REAL-NS 2); :: thesis: ( z = x + (y * <i> ) & v = <*x,y*> implies |.z.| = ||.v.|| )
assume A1: ( z = x + (y * <i> ) & v = <*x,y*> ) ; :: thesis: |.z.| = ||.v.||
reconsider xx = <*x,y*> as Element of REAL 2 by FINSEQ_2:121;
reconsider xx1 = xx as Point of (TOP-REAL 2) by EUCLID:25;
A3: xx1 `1 = x by FINSEQ_1:61;
A4: xx1 `2 = y by FINSEQ_1:61;
A5: len (sqr xx) = 2 by FINSEQ_1:def 18;
A6: (sqr xx) . 1 = x ^2 by A3, VALUED_1:11;
(sqr xx) . 2 = y ^2 by A4, VALUED_1:11;
then A2: sqr xx = <*(x ^2 ),(y ^2 )*> by A5, A6, FINSEQ_1:61;
A8: |.xx.| = ||.v.|| by A1, REAL_NS1:1;
( Re z = x & Im z = y ) by A1, COMPLEX1:28;
hence |.z.| = ||.v.|| by A2, A8, RVSUM_1:107; :: thesis: verum