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