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