let S1, S2, S3 be non empty ManySortedSign ; :: thesis: for f1, g1, f2, g2 being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2
for C3 being non-empty MSAlgebra over S3 st C1,C2 are_similar_wrt f1,g1 & C2,C3 are_similar_wrt f2,g2 holds
C1,C3 are_similar_wrt f2 * f1,g2 * g1
let f1, g1, f2, g2 be Function; :: thesis: for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2
for C3 being non-empty MSAlgebra over S3 st C1,C2 are_similar_wrt f1,g1 & C2,C3 are_similar_wrt f2,g2 holds
C1,C3 are_similar_wrt f2 * f1,g2 * g1
let C1 be non-empty MSAlgebra over S1; :: thesis: for C2 being non-empty MSAlgebra over S2
for C3 being non-empty MSAlgebra over S3 st C1,C2 are_similar_wrt f1,g1 & C2,C3 are_similar_wrt f2,g2 holds
C1,C3 are_similar_wrt f2 * f1,g2 * g1
let C2 be non-empty MSAlgebra over S2; :: thesis: for C3 being non-empty MSAlgebra over S3 st C1,C2 are_similar_wrt f1,g1 & C2,C3 are_similar_wrt f2,g2 holds
C1,C3 are_similar_wrt f2 * f1,g2 * g1
let C3 be non-empty MSAlgebra over S3; :: thesis: ( C1,C2 are_similar_wrt f1,g1 & C2,C3 are_similar_wrt f2,g2 implies C1,C3 are_similar_wrt f2 * f1,g2 * g1 )
assume that
A1: f1,g1 form_embedding_of C1,C2 and
A2: f1 " ,g1 " form_embedding_of C2,C1 and
A3: f2,g2 form_embedding_of C2,C3 and
A4: f2 " ,g2 " form_embedding_of C3,C2 ; :: according to CIRCTRM1:def 13 :: thesis: C1,C3 are_similar_wrt f2 * f1,g2 * g1
thus f2 * f1,g2 * g1 form_embedding_of C1,C3 by A1, A3, Th35; :: according to CIRCTRM1:def 13 :: thesis: (f2 * f1) " ,(g2 * g1) " form_embedding_of C3,C1
A5: f1 is one-to-one by A1;
A6: g1 is one-to-one by A1;
A7: f2 is one-to-one by A3;
A8: g2 is one-to-one by A3;
A9: (f2 * f1) " = (f1 ") * (f2 ") by A5, A7, FUNCT_1:44;
(g2 * g1) " = (g1 ") * (g2 ") by A6, A8, FUNCT_1:44;
hence (f2 * f1) " ,(g2 * g1) " form_embedding_of C3,C1 by A2, A4, A9, Th35; :: thesis: verum