:: deftheorem Def22 defines ProdOpSeq PRALG_1:def 24 :
for J being non empty set
for A being Univ_Alg-yielding equal-signature ManySortedSet of J
for b₃ being PFuncFinSequence of (product (Carrier A)) holds
( b₃ = ProdOpSeq A iff ( len b₃ = len (ComSign A) & ( for n being Nat st n in dom b₃ holds
b₃ . n = [[:(ProdOp (A,n)):]] ) ) );