:: deftheorem Def1 defines InnerProduct MFOLD_2:def 1 :
for n being Nat
for p being Point of (TOP-REAL n)
for b₃ being Function of (TOP-REAL n),R^1 holds
( b₃ = InnerProduct p iff for q being Point of (TOP-REAL n) holds b₃ . q = |(p,q)| );