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
C2,C1 are_similar_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
C2,C1 are_similar_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
C2,C1 are_similar_wrt f " ,g "
let C2 be non-empty MSAlgebra of S2; :: thesis: ( C1,C2 are_similar_wrt f,g implies C2,C1 are_similar_wrt f " ,g " )
assume A1: ( f,g form_embedding_of C1,C2 & f " ,g " form_embedding_of C2,C1 ) ; :: according to CIRCTRM1:def 13 :: thesis: C2,C1 are_similar_wrt f " ,g "
then ( f is one-to-one & g is one-to-one ) by Def12;
then ( (f " ) " = f & (g " ) " = g ) by FUNCT_1:65;
hence ( f " ,g " form_embedding_of C2,C1 & (f " ) " ,(g " ) " form_embedding_of C1,C2 ) by A1; :: according to CIRCTRM1:def 13 :: thesis: verum