let S1, S2, S3 be non empty ManySortedSign ; :: thesis: for f1, g1, f2, g2 being Function
for C1 being non-empty MSAlgebra of S1
for C2 being non-empty MSAlgebra of S2
for C3 being non-empty MSAlgebra of 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 of S1
for C2 being non-empty MSAlgebra of S2
for C3 being non-empty MSAlgebra of 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 of S1; :: thesis: for C2 being non-empty MSAlgebra of S2
for C3 being non-empty MSAlgebra of 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 of S2; :: thesis: for C3 being non-empty MSAlgebra of 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 of 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, Th36; :: according to CIRCTRM1:def 13 :: thesis: (f2 * f1) " ,(g2 * g1) " form_embedding_of C3,C1
A5: f1 is one-to-one by A1, Def12;
A6: g1 is one-to-one by A1, Def12;
A7: f2 is one-to-one by A3, Def12;
A8: g2 is one-to-one by A3, Def12;
A9: (f2 * f1) " = (f1 " ) * (f2 " ) by A5, A7, FUNCT_1:66;
(g2 * g1) " = (g1 " ) * (g2 " ) by A6, A8, FUNCT_1:66;
hence (f2 * f1) " ,(g2 * g1) " form_embedding_of C3,C1 by A2, A4, A9, Th36; :: thesis: verum