let n be Nat; :: thesis: for x1 being Point of (REAL-NS n)
for x2 being Point of (REAL-US n) st x1 = x2 holds
||.x1.|| ^2 = x2 .|. x2
let x1 be Point of (REAL-NS n); :: thesis: for x2 being Point of (REAL-US n) st x1 = x2 holds
||.x1.|| ^2 = x2 .|. x2
let x2 be Point of (REAL-US n); :: thesis: ( x1 = x2 implies ||.x1.|| ^2 = x2 .|. x2 )
reconsider x = x1 as Element of REAL n by Def4;
assume A1: x1 = x2 ; :: thesis: ||.x1.|| ^2 = x2 .|. x2
thus ||.x1.|| ^2 = |.x.| ^2 by Th1
.= |(x,x)| by EUCLID_2:4
.= Sum (mlt (x,x)) by RVSUM_1:def 16
.= (Euclid_scalar n) . (x,x) by Def5
.= x2 .|. x2 by A1, Def6 ; :: thesis: verum