let S be non void Signature; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 Th31;
then A3: the carrier of S -indexing f,g form_a_replacement_in S by A1, Th31;
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; :: thesis: verum