:: deftheorem Def14 defines ComSign PRALG_1:def 16 :
for J being non empty set
for A being Univ_Alg-yielding equal-signature ManySortedSet of J
for b₃ being FinSequence of NAT holds
( b₃ = ComSign A iff for j being Element of J holds b₃ = signature (A . j) );