:: deftheorem Def4 defines with-replacement ALGSPEC1:def 4 :
for S being non empty non void ManySortedSign
for f, g being Function st f,g form_a_replacement_in S holds
for b₄ being non empty non void strict ManySortedSign holds
( b₄ = S with-replacement (f,g) iff ( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b₄ & the carrier of b₄ = rng ( the carrier of S -indexing f) & the carrier' of b₄ = rng ( the carrier' of S -indexing g) ) );