let n be Element of 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 )
assume A1: x1 = x2 ; :: thesis: ||.x1.|| ^2 = x2 .|. x2
reconsider x = x1 as Element of REAL n by Def4;
thus ||.x1.|| ^2 = |.x.| ^2 by Th1
.= |(x,x)| by EUCLID_2:12
.= Sum (mlt x,x) by EUCLID_2:def 1
.= (Euclid_scalar n) . x,x by Def5
.= x2 .|. x2 by A1, Def6 ; :: thesis: verum