theorem Th40: :: ALGSPEC1:40

for S being non void Signature
for f, g being Function holds
( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) ) by Th30, Th31, Def4;