let S be non void Signature; :: thesis: for f, g being Function st f,g form_a_replacement_in S holds
the carrier of S -indexing f is Function of the carrier of S, the carrier of (S with-replacement (f,g))
let f, g be Function; :: thesis: ( f,g form_a_replacement_in S implies the carrier of S -indexing f is Function of the carrier of S, the carrier of (S with-replacement (f,g)) )
assume f,g form_a_replacement_in S ; :: thesis: the carrier of S -indexing f is Function of the carrier of S, the carrier of (S with-replacement (f,g))
then the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) by Def4;
hence the carrier of S -indexing f is Function of the carrier of S, the carrier of (S with-replacement (f,g)) by INSTALG1:9; :: thesis: verum