let S be non empty non void ManySortedSign ; :: thesis: S is_rougher_than S
take f = id the carrier of S; :: according to PUA2MSS1:def 13 :: thesis: ex g being Function st
( f,g form_morphism_between S,S & rng f = the carrier of S & rng g = the carrier' of S )
take g = id the carrier' of S; :: thesis: ( f,g form_morphism_between S,S & rng f = the carrier of S & rng g = the carrier' of S )
thus ( f,g form_morphism_between S,S & rng f = the carrier of S & rng g = the carrier' of S ) by Th29, RELAT_1:45; :: thesis: verum