theorem Th24: :: CIRCTRM1:24

for S1, S2 being non empty ManySortedSign
for f, g being Function st S1,S2 are_equivalent_wrt f,g holds
( rng f = the carrier of S2 & rng g = the carrier' of S2 )