theorem Th41: :: ALGSPEC1:41

for S being non void Signature
for f, g being Function st dom f c= the carrier of S & dom g c= the carrier' of S & f,g form_a_replacement_in S holds
(id the carrier of S) +* f,(id the carrier' of S) +* g form_morphism_between S,S with-replacement (f,g)