for S1, S2 being ManySortedSign
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 ) by FUNCT_2:2;