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