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