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