theorem Th44: :: ALGSPEC1:44

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