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

||.vx.|| = |.x.|

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

( x in REAL & 0 in REAL ) by XREAL_0:def 1;

then reconsider xx = <*x,0*> as Element of REAL 2 by FINSEQ_2:101;

reconsider xx1 = xx as Point of (TOP-REAL 2) by EUCLID:22;

assume vx = <*x,0*> ; :: thesis: ||.vx.|| = |.x.|

then A1: ||.vx.|| = |.xx.| by REAL_NS1:1;

xx1 `2 = 0 by FINSEQ_1:44;

then A2: (sqr xx) . 2 = 0 ^2 by VALUED_1:11;

xx1 `1 = x by FINSEQ_1:44;

then ( len (sqr xx) = 2 & (sqr xx) . 1 = x ^2 ) by CARD_1:def 7, VALUED_1:11;

then sqr xx = <*(x ^2),(0 ^2)*> by A2, FINSEQ_1:44;

then sqrt (Sum (sqr xx)) = sqrt ((x ^2) + (0 ^2)) by RVSUM_1:77

.= sqrt ((x ^2) + (0 * 0)) by SQUARE_1:def 1 ;

hence ||.vx.|| = |.x.| by A1, COMPLEX1:72; :: thesis: verum

||.vx.|| = |.x.|

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

( x in REAL & 0 in REAL ) by XREAL_0:def 1;

then reconsider xx = <*x,0*> as Element of REAL 2 by FINSEQ_2:101;

reconsider xx1 = xx as Point of (TOP-REAL 2) by EUCLID:22;

assume vx = <*x,0*> ; :: thesis: ||.vx.|| = |.x.|

then A1: ||.vx.|| = |.xx.| by REAL_NS1:1;

xx1 `2 = 0 by FINSEQ_1:44;

then A2: (sqr xx) . 2 = 0 ^2 by VALUED_1:11;

xx1 `1 = x by FINSEQ_1:44;

then ( len (sqr xx) = 2 & (sqr xx) . 1 = x ^2 ) by CARD_1:def 7, VALUED_1:11;

then sqr xx = <*(x ^2),(0 ^2)*> by A2, FINSEQ_1:44;

then sqrt (Sum (sqr xx)) = sqrt ((x ^2) + (0 ^2)) by RVSUM_1:77

.= sqrt ((x ^2) + (0 * 0)) by SQUARE_1:def 1 ;

hence ||.vx.|| = |.x.| by A1, COMPLEX1:72; :: thesis: verum