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 A1: 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 A2: ( dom f = the carrier of S1 & rng f c= the carrier of S2 ) by PUA2MSS1:def 13;
( dom g = the carrier' of S1 & rng g c= the carrier' of S2 ) by A1, 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 A2, FUNCT_2:4; :: thesis: verum