let S1, S2, S3 be non empty ManySortedSign ; :: thesis: ( S1,S2 are_equivalent & S2,S3 are_equivalent implies S1,S3 are_equivalent )
given f1, g1 being one-to-one Function such that A1: S1,S2 are_equivalent_wrt f1,g1 ; :: according to CIRCTRM1:def 10 :: thesis: ( not S2,S3 are_equivalent or S1,S3 are_equivalent )
given f2, g2 being one-to-one Function such that A2: S2,S3 are_equivalent_wrt f2,g2 ; :: according to CIRCTRM1:def 10 :: thesis: S1,S3 are_equivalent
take f2 * f1 ; :: according to CIRCTRM1:def 10 :: thesis: ex g being one-to-one Function st S1,S3 are_equivalent_wrt f2 * f1,g
take g2 * g1 ; :: thesis: S1,S3 are_equivalent_wrt f2 * f1,g2 * g1
thus S1,S3 are_equivalent_wrt f2 * f1,g2 * g1 by A1, A2, Th27; :: thesis: verum