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

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