theorem :: EUCLID_7:38

for n being Nat
for u, v being Element of REAL n holds (Euclid_scalar n) . (u,v) = |(u,v)| by REAL_NS1:def 5;