:: deftheorem defines form_morphism_between PUA2MSS1:def 12 :
for S1, S2 being ManySortedSign
for f, g being Function holds
( f,g form_morphism_between S1,S2 iff ( dom f = the carrier of S1 & dom g = the carrier' of S1 & rng f c= the carrier of S2 & rng g c= the carrier' of S2 & f * the ResultSort of S1 = the ResultSort of S2 * g & ( for o being set
for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
f * p = the Arity of S2 . (g . o) ) ) );