:: deftheorem defines are_equivalent_wrt CIRCTRM1:def 9 :
for S1, S2 being non empty ManySortedSign
for f, g being Function holds
( S1,S2 are_equivalent_wrt f,g iff ( f is one-to-one & g is one-to-one & f,g form_morphism_between S1,S2 & f " ,g " form_morphism_between S2,S1 ) );