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 A1: ( f1,g1 form_embedding_of C1,C2 & f1 " ,g1 " form_embedding_of C2,C1 & f2,g2 form_embedding_of C2,C3 & f2 " ,g2 " form_embedding_of C3,C2 ) ; :: according to CIRCTRM1:def 13 :: thesis: C1,C3 are_similar_wrt f2 * f1,g2 * g1
hence f2 * f1,g2 * g1 form_embedding_of C1,C3 by Th36; :: according to CIRCTRM1:def 13 :: thesis: (f2 * f1) " ,(g2 * g1) " form_embedding_of C3,C1
( f1 is one-to-one & g1 is one-to-one & f2 is one-to-one & g2 is one-to-one ) by A1, Def12;
then ( (f2 * f1) " = (f1 " ) * (f2 " ) & (g2 * g1) " = (g1 " ) * (g2 " ) ) by FUNCT_1:66;
hence (f2 * f1) " ,(g2 * g1) " form_embedding_of C3,C1 by A1, Th36; :: thesis: verum