let S1, S2 be non empty ManySortedSign ; :: thesis: for f, g being Function
for C1 being non-empty MSAlgebra of S1
for C2 being non-empty MSAlgebra of S2 st C1,C2 are_similar_wrt f,g holds
S1,S2 are_equivalent_wrt f,g
let f, g be Function; :: thesis: for C1 being non-empty MSAlgebra of S1
for C2 being non-empty MSAlgebra of S2 st C1,C2 are_similar_wrt f,g holds
S1,S2 are_equivalent_wrt f,g
let C1 be non-empty MSAlgebra of S1; :: thesis: for C2 being non-empty MSAlgebra of S2 st C1,C2 are_similar_wrt f,g holds
S1,S2 are_equivalent_wrt f,g
let C2 be non-empty MSAlgebra of S2; :: thesis: ( C1,C2 are_similar_wrt f,g implies S1,S2 are_equivalent_wrt f,g )
assume ( f is one-to-one & g is one-to-one & f,g form_morphism_between S1,S2 & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g & f " is one-to-one & g " is one-to-one & f " ,g " form_morphism_between S2,S1 ) ; :: according to CIRCTRM1:def 12,CIRCTRM1:def 13 :: thesis: ( not the Sorts of C2 = the Sorts of C1 * (f " ) or not the Charact of C2 = the Charact of C1 * (g " ) or S1,S2 are_equivalent_wrt f,g )
hence ( not the Sorts of C2 = the Sorts of C1 * (f " ) or not the Charact of C2 = the Charact of C1 * (g " ) or S1,S2 are_equivalent_wrt f,g ) by Def9; :: thesis: verum