for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
for g9 being rng-retract of the carrier' of S -indexing g holds the ResultSort of (S with-replacement (f,g)) = (( the carrier of S -indexing f) * the ResultSort of S) * g9