let S1, S2, S3 be non empty ManySortedSign ; :: thesis: for f1, g1, f2, g2 being Function st S1,S2 are_equivalent_wrt f1,g1 & S2,S3 are_equivalent_wrt f2,g2 holds
S1,S3 are_equivalent_wrt f2 * f1,g2 * g1
let f1, g1, f2, g2 be Function; :: thesis: ( S1,S2 are_equivalent_wrt f1,g1 & S2,S3 are_equivalent_wrt f2,g2 implies S1,S3 are_equivalent_wrt f2 * f1,g2 * g1 )
assume that
A1: f1 is one-to-one and
A2: g1 is one-to-one and
A3: f1,g1 form_morphism_between S1,S2 and
A4: f1 " ,g1 " form_morphism_between S2,S1 and
A5: f2 is one-to-one and
A6: g2 is one-to-one and
A7: f2,g2 form_morphism_between S2,S3 and
A8: f2 " ,g2 " form_morphism_between S3,S2 ; :: according to CIRCTRM1:def 9 :: thesis: S1,S3 are_equivalent_wrt f2 * f1,g2 * g1
thus ( f2 * f1 is one-to-one & g2 * g1 is one-to-one ) by A1, A2, A5, A6; :: according to CIRCTRM1:def 9 :: thesis: ( f2 * f1,g2 * g1 form_morphism_between S1,S3 & (f2 * f1) " ,(g2 * g1) " form_morphism_between S3,S1 )
A9: (f2 * f1) " = (f1 ") * (f2 ") by A1, A5, FUNCT_1:44;
(g2 * g1) " = (g1 ") * (g2 ") by A2, A6, FUNCT_1:44;
hence ( f2 * f1,g2 * g1 form_morphism_between S1,S3 & (f2 * f1) " ,(g2 * g1) " form_morphism_between S3,S1 ) by A3, A4, A7, A8, A9, PUA2MSS1:29; :: thesis: verum