for S1, S2, S3 being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S3
for f1 being Function of the carrier of S1, the carrier of S2
for g1 being Function st f1,g1 form_morphism_between S1,S2 holds
for f2 being Function of the carrier of S2, the carrier of S3
for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2))