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:10; :: thesis: verum