for S, S9 being non void Signature
for f, g being Function st f,g form_morphism_between S,S9 holds
f,g form_a_replacement_in S