:: deftheorem Def1 defines product PRVECT_1:def 1 :
for D being non empty set
for F being BinOp of D
for n being Nat
for b₄ being BinOp of (n -tuples_on D) holds
( b₄ = product (F,n) iff for x, y being Element of n -tuples_on D holds b₄ . (x,y) = F .: (x,y) );