let S1, S2, S3 be ManySortedSign ; :: thesis: ( S1 is_rougher_than S2 & S2 is_rougher_than S3 implies S1 is_rougher_than S3 )
given f1, g1 being Function such that A1: f1,g1 form_morphism_between S2,S1 and
A2: rng f1 = the carrier of S1 and
A3: rng g1 = the carrier' of S1 ; :: according to PUA2MSS1:def 13 :: thesis: ( not S2 is_rougher_than S3 or S1 is_rougher_than S3 )
given f2, g2 being Function such that A4: f2,g2 form_morphism_between S3,S2 and
A5: rng f2 = the carrier of S2 and
A6: rng g2 = the carrier' of S2 ; :: according to PUA2MSS1:def 13 :: thesis: S1 is_rougher_than S3
take f = f1 * f2; :: according to PUA2MSS1:def 13 :: thesis: ex g being Function st
( f,g form_morphism_between S3,S1 & rng f = the carrier of S1 & rng g = the carrier' of S1 )
take g = g1 * g2; :: thesis: ( f,g form_morphism_between S3,S1 & rng f = the carrier of S1 & rng g = the carrier' of S1 )
thus f,g form_morphism_between S3,S1 by A1, A4, Th28; :: thesis: ( rng f = the carrier of S1 & rng g = the carrier' of S1 )
A7: dom f1 = the carrier of S2 by A1;
dom g1 = the carrier' of S2 by A1;
hence ( rng f = the carrier of S1 & rng g = the carrier' of S1 ) by A2, A3, A5, A6, A7, RELAT_1:28; :: thesis: verum