let S1, S2 be non empty ManySortedSign ; :: thesis: for f, g being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over 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 over S1
for C2 being non-empty MSAlgebra over S2 st C1,C2 are_similar_wrt f,g holds
S1,S2 are_equivalent_wrt f,g
let C1 be non-empty MSAlgebra over S1; :: thesis: for C2 being non-empty MSAlgebra over S2 st C1,C2 are_similar_wrt f,g holds
S1,S2 are_equivalent_wrt f,g
let C2 be non-empty MSAlgebra over S2; :: thesis: ( C1,C2 are_similar_wrt f,g implies S1,S2 are_equivalent_wrt f,g )
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: f,g form_morphism_between S1,S2 and
the Sorts of C1 = the Sorts of C2 * f and
the Charact of C1 = the Charact of C2 * g and
f " is one-to-one and
g " is one-to-one and
A4: 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 )
thus ( 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 A1, A2, A3, A4; :: thesis: verum