let S be non void Signature; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum