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

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

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

reconsider xx = vx as Element of REAL 1 by REAL_NS1:def 4;

reconsider x2 = x ^2 as Element of REAL by XREAL_0:def 1;

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

then sqrt (Sum (sqr xx)) = sqrt (Sum <*x2*>) by RVSUM_1:55;

then A1: sqrt (Sum (sqr xx)) = sqrt (x ^2) by RVSUM_1:73;

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

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

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

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

reconsider xx = vx as Element of REAL 1 by REAL_NS1:def 4;

reconsider x2 = x ^2 as Element of REAL by XREAL_0:def 1;

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

then sqrt (Sum (sqr xx)) = sqrt (Sum <*x2*>) by RVSUM_1:55;

then A1: sqrt (Sum (sqr xx)) = sqrt (x ^2) by RVSUM_1:73;

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

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