for A being partial non-empty UAStr
for S being non empty non void ManySortedSign
for G being MSAlgebra over S
for Q being IndexedPartition of the carrier' of S st A can_be_characterized_by S,G,Q holds
for o being OperSymbol of A
for r being FinSequence of rng the Sorts of G st product r c= dom (Den (o,A)) holds
ex s being OperSymbol of S st
( the Sorts of G * (the_arity_of s) = r & s in Q . o )