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 & g1 is one-to-one ) and
A2: f1,g1 form_morphism_between S1,S2 and
A3: f1 " ,g1 " form_morphism_between S2,S1 and
A4: ( f2 is one-to-one & g2 is one-to-one ) and
A5: f2,g2 form_morphism_between S2,S3 and
A6: 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, A4; :: according to CIRCTRM1:def 9 :: thesis: ( f2 * f1,g2 * g1 form_morphism_between S1,S3 & (f2 * f1) " ,(g2 * g1) " form_morphism_between S3,S1 )
( (f2 * f1) " = (f1 " ) * (f2 " ) & (g2 * g1) " = (g1 " ) * (g2 " ) ) by A1, A4, FUNCT_1:66;
hence ( f2 * f1,g2 * g1 form_morphism_between S1,S3 & (f2 * f1) " ,(g2 * g1) " form_morphism_between S3,S1 ) by A2, A3, A5, A6, PUA2MSS1:30; :: thesis: verum