let x be Real; :: thesis: for vx being Element of (REAL-NS 2) st vx = <*0 ,x*> holds
||.vx.|| = abs x
let vx be Element of (REAL-NS 2); :: thesis: ( vx = <*0 ,x*> implies ||.vx.|| = abs x )
assume A1: vx = <*0 ,x*> ; :: thesis: ||.vx.|| = abs x
reconsider xx = <*0 ,x*> as Element of REAL 2 by FINSEQ_2:121;
reconsider xx1 = xx as Point of (TOP-REAL 2) by EUCLID:25;
A3: xx1 `1 = 0 by FINSEQ_1:61;
A4: xx1 `2 = x by FINSEQ_1:61;
A5: len (sqr xx) = 2 by FINSEQ_1:def 18;
A6: (sqr xx) . 1 = 0 ^2 by A3, VALUED_1:11;
(sqr xx) . 2 = x ^2 by A4, VALUED_1:11;
then sqr xx = <*(0 ^2 ),(x ^2 )*> by A5, A6, FINSEQ_1:61;
then A2: sqrt (Sum (sqr xx)) = sqrt ((0 ^2 ) + (x ^2 )) by RVSUM_1:107
.= sqrt ((0 * 0 ) + (x ^2 )) by SQUARE_1:def 3
.= sqrt (x ^2 ) ;
||.vx.|| = |.xx.| by A1, REAL_NS1:1;
hence ||.vx.|| = abs x by A2, COMPLEX1:158; :: thesis: verum