for f, g being Function
for S being non void Signature
for E being Extension of S st f,g form_a_replacement_in E holds
E with-replacement (f,g) is Extension of S with-replacement (f,g)