for S1, S2 being ManySortedSign st ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) holds
for o, a being set
for r1 being Element of S1
for r2 being Element of S2 st r1 = r2 & o is_of_type a,r1 holds
o is_of_type a,r2 ;