let S be non void Signature; :: thesis: for f, g being Function st f,g form_a_replacement_in S holds
for g9 being rng-retract of the carrier' of S -indexing g holds the ResultSort of (S with-replacement f,g) = ((the carrier of S -indexing f) * the ResultSort of S) * g9
let f, g be Function; :: thesis: ( f,g form_a_replacement_in S implies for g9 being rng-retract of the carrier' of S -indexing g holds the ResultSort of (S with-replacement f,g) = ((the carrier of S -indexing f) * the ResultSort of S) * g9 )
set ff = the carrier of S -indexing f;
set gg = the carrier' of S -indexing g;
set T = S with-replacement f,g;
assume A1: f,g form_a_replacement_in S ; :: thesis: for g9 being rng-retract of the carrier' of S -indexing g holds the ResultSort of (S with-replacement f,g) = ((the carrier of S -indexing f) * the ResultSort of S) * g9
then A2: the carrier of S -indexing f,the carrier' of S -indexing g form_morphism_between S,S with-replacement f,g by Def4;
let g9 be rng-retract of the carrier' of S -indexing g; :: thesis: the ResultSort of (S with-replacement f,g) = ((the carrier of S -indexing f) * the ResultSort of S) * g9
the carrier' of (S with-replacement f,g) = rng (the carrier' of S -indexing g) by A1, Def4;
hence the ResultSort of (S with-replacement f,g) = the ResultSort of (S with-replacement f,g) * (id (rng (the carrier' of S -indexing g))) by FUNCT_2:23
.= the ResultSort of (S with-replacement f,g) * ((the carrier' of S -indexing g) * g9) by Def2
.= (the ResultSort of (S with-replacement f,g) * (the carrier' of S -indexing g)) * g9 by RELAT_1:55
.= ((the carrier of S -indexing f) * the ResultSort of S) * g9 by A2, PUA2MSS1:def 13 ;
:: thesis: verum