:: deftheorem Def4 defines -Mult_over PRVECT_1:def 4 :
for F being Field
for n being Nat
for b₃ being Function of [: the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F) holds
( b₃ = n -Mult_over F iff for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b₃ . (x,v) = the multF of F [;] (x,v) );