:: deftheorem Def2 defines product PRVECT_1:def 2 :
for D being non empty set
for F being UnOp of D
for n being Nat
for b₄ being UnOp of (n -tuples_on D) holds
( b₄ = product (F,n) iff for x being Element of n -tuples_on D holds b₄ . x = F * x );