:: deftheorem defines are_similar CIRCTRM1:def 14 :
for S1, S2 being non empty ManySortedSign
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 holds
( C1,C2 are_similar iff ex f, g being Function st C1,C2 are_similar_wrt f,g );