for S being ManySortedSign
for T being feasible ManySortedSign
for T9 being Subsignature of T
for f, g being Function st f,g form_morphism_between S,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds
f,g form_morphism_between S,T9