for S1, S2, S being non empty ManySortedSign
for f1, g1, f2, g2 being Function st f1 tolerates f2 & f1,g1 form_morphism_between S1,S & f2,g2 form_morphism_between S2,S holds
f1 +* f2,g1 +* g2 form_morphism_between S1 +* S2,S