let S1, S2 be ManySortedSign ; :: thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
( f is Function of the carrier of S1,the carrier of S2 & g is Function of the carrier' of S1,the carrier' of S2 )
let f, g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies ( f is Function of the carrier of S1,the carrier of S2 & g is Function of the carrier' of S1,the carrier' of S2 ) )
assume f,g form_morphism_between S1,S2 ; :: thesis: ( f is Function of the carrier of S1,the carrier of S2 & g is Function of the carrier' of S1,the carrier' of S2 )
then ( dom g = the carrier' of S1 & rng g c= the carrier' of S2 & dom f = the carrier of S1 & rng f c= the carrier of S2 ) by PUA2MSS1:def 13;
hence ( f is Function of the carrier of S1,the carrier of S2 & g is Function of the carrier' of S1,the carrier' of S2 ) by FUNCT_2:4; :: thesis: verum