:: deftheorem Def14 defines MSSign PUA2MSS1:def 14 :
for A being partial non-empty UAStr
for P being a_partition of A
for b₃ being strict ManySortedSign holds
( b₃ = MSSign (A,P) iff ( the carrier of b₃ = P & the carrier' of b₃ = { [o,p] where o is OperSymbol of A, p is Element of P * : product p meets dom (Den (o,A)) } & ( for o being OperSymbol of A
for p being Element of P * st product p meets dom (Den (o,A)) holds
( the Arity of b₃ . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b₃ . [o,p] ) ) ) );