let n be Nat; :: thesis: for x being VECTOR of (REAL-NS n)
for y being Element of REAL n st x = y holds
||.x.|| = |.y.|
let x be VECTOR of (REAL-NS n); :: thesis: for y being Element of REAL n st x = y holds
||.x.|| = |.y.|
let y be Element of REAL n; :: thesis: ( x = y implies ||.x.|| = |.y.| )
assume A1: x = y ; :: thesis: ||.x.|| = |.y.|
thus ||.x.|| = the normF of (REAL-NS n) . x
.= (Euclid_norm n) . y by A1, Def4
.= |.y.| by Def3 ; :: thesis: verum