:: deftheorem Def5 defines prodTuples POLYNOM3:def 5 :
for L being non empty multMagma
for p, q, r being sequence of L
for t being FinSequence of 3 -tuples_on NAT
for b₆ being Element of the carrier of L * holds
( b₆ = prodTuples (p,q,r,t) iff ( len b₆ = len t & ( for k being Element of NAT st k in dom t holds
b₆ . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) ) );