:: deftheorem defines are_equivalent CIRCTRM1:def 10 :
for S1, S2 being non empty ManySortedSign holds
( S1,S2 are_equivalent iff ex f, g being one-to-one Function st S1,S2 are_equivalent_wrt f,g );