:: deftheorem defines can_be_characterized_by PUA2MSS1:def 15 :
for A being partial non-empty UAStr
for S being non empty non void ManySortedSign
for G being MSAlgebra over S
for P being IndexedPartition of the carrier' of S holds
( A can_be_characterized_by S,G,P iff ( the Sorts of G is IndexedPartition of A & dom P = dom the charact of A & ( for o being OperSymbol of A holds the Charact of G | (P . o) is IndexedPartition of Den (o,A) ) ) );