let S be non void Signature; :: thesis: for f, g being Function holds
( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) )
let f, g be Function; :: thesis: ( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) )
set ff = the carrier of S -indexing f;
set gg = the carrier' of S -indexing g;
set S9 = S with-replacement (f,g);
thus ( f,g form_a_replacement_in S implies the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) ) by Def4; :: thesis: ( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) implies f,g form_a_replacement_in S )
assume the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) ; :: thesis: f,g form_a_replacement_in S
then the carrier of S -indexing f, the carrier' of S -indexing g form_a_replacement_in S by Th32;
hence f,g form_a_replacement_in S by Th31; :: thesis: verum