let x be Real; :: thesis: for vx being Element of (REAL-NS 1) st vx = <*x*> holds
||.vx.|| = abs x
let vx be Element of (REAL-NS 1); :: thesis: ( vx = <*x*> implies ||.vx.|| = abs x )
assume A1: vx = <*x*> ; :: thesis: ||.vx.|| = abs x
reconsider xx = vx as Element of REAL 1 by REAL_NS1:def 4;
sqrt (Sum (sqr xx)) = sqrt (Sum <*(x ^2 )*>) by A1, RVSUM_1:81;
then A2: sqrt (Sum (sqr xx)) = sqrt (x ^2 ) by RVSUM_1:103;
||.vx.|| = |.xx.| by REAL_NS1:1;
hence ||.vx.|| = abs x by A2, COMPLEX1:158; :: thesis: verum