:: deftheorem Def2 defines Euclid_mult REAL_NS1:def 2 :
for n being Nat
for b₂ being Function of [:REAL,(REAL n):],(REAL n) holds
( b₂ = Euclid_mult n iff for r being Real
for x being Element of REAL n holds b₂ . (r,x) = r * x );