let S1, S2, S3 be ManySortedSign ; ( 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
; PUA2MSS1:def 13 ( 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
; PUA2MSS1:def 13 S1 is_rougher_than S3
take f = f1 * f2; PUA2MSS1:def 13 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; ( 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; ( 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; verum