for S, S9 being non void Signature
for f, g being Function st f,g form_morphism_between S,S9 holds
S with-replacement (f,g) is Subsignature of S9