let S be non empty non void ManySortedSign ; :: thesis: (S,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 Th27; :: thesis: verum