let S be non void Signature; :: thesis: for f, g being Function st f,g form_a_replacement_in S holds
for g' 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) * g'
let f, g be Function; :: thesis: ( f,g form_a_replacement_in S implies for g' 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) * g' )
set ff = the carrier of S -indexing f;
set gg = the carrier' of S -indexing g;
set T = S with-replacement f,g;
assume f,g form_a_replacement_in S ; :: thesis: for g' 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) * g'
then A1: ( the carrier of S -indexing f,the carrier' of S -indexing g form_morphism_between S,S with-replacement f,g & the carrier of (S with-replacement f,g) = rng (the carrier of S -indexing f) & the carrier' of (S with-replacement f,g) = rng (the carrier' of S -indexing g) ) by Def4;
let g' 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) * g'
thus 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 A1, FUNCT_2:23
.= the ResultSort of (S with-replacement f,g) * ((the carrier' of S -indexing g) * g') by Def2
.= (the ResultSort of (S with-replacement f,g) * (the carrier' of S -indexing g)) * g' by RELAT_1:55
.= ((the carrier of S -indexing f) * the ResultSort of S) * g' by A1, PUA2MSS1:def 13 ; :: thesis: verum