for S1, S2 being non void Signature
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
(f *) * the Arity of S1 = the Arity of S2 * g