let S be 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)
let f, g be Function; ( f,g form_a_replacement_in S implies S with-replacement (f,( the carrier' of S -indexing g)) = S with-replacement (f,g) )
set X = the carrier of S;
set Y = the carrier' of S;
set S2 = S with-replacement (f,( the carrier' of S -indexing g));
A1:
the carrier' of S -indexing ( the carrier' of S -indexing g) = the carrier' of S -indexing g
by Th11;
assume A2:
f,g form_a_replacement_in S
; S with-replacement (f,( the carrier' of S -indexing g)) = S with-replacement (f,g)
then
the carrier of S -indexing f, the carrier' of S -indexing g form_a_replacement_in S
by Th30;
then A3:
f, the carrier' of S -indexing g form_a_replacement_in S
by A1, Th30;
then A4:
the carrier' of (S with-replacement (f,( the carrier' of S -indexing g))) = rng ( the carrier' of S -indexing g)
by A1, Def4;
A5:
the carrier of (S with-replacement (f,( the carrier' of S -indexing g))) = rng ( the carrier of S -indexing f)
by A3, Def4;
the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,( the carrier' of S -indexing g))
by A1, A3, Def4;
hence
S with-replacement (f,( the carrier' of S -indexing g)) = S with-replacement (f,g)
by A2, A5, A4, Def4; verum