:: deftheorem Def5 defines Euclid_scalar REAL_NS1:def 5 :
for n being Nat
for b₂ being Function of [:(REAL n),(REAL n):],REAL holds
( b₂ = Euclid_scalar n iff for x, y being Element of REAL n holds b₂ . (x,y) = Sum (mlt (x,y)) );