let S, S9 be non void Signature; :: thesis:
let f, g be Function; :: thesis:
set R = S with-replacement (f,g);
set F = id the carrier of (S with-replacement (f,g));
set G = id the carrier' of (S with-replacement (f,g));
set f9 = the carrier of S -indexing f;
set g9 = the carrier' of S -indexing g;
A1: dom the ResultSort of S9 = the carrier' of S9 by FUNCT_2:def 1;
A2: dom the ResultSort of (S with-replacement (f,g)) = the carrier' of (S with-replacement (f,g)) by FUNCT_2:def 1;
assume A3: f,g form_morphism_between S,S9 ; :: thesis:
then dom f = the carrier of S ;
then A4: the carrier of S -indexing f = f by Th10;
A5: f,g form_a_replacement_in S by A3, Th31;
then A6: the carrier' of (S with-replacement (f,g)) = rng ( the carrier' of S -indexing g) by Def4;
thus ( dom (id the carrier of (S with-replacement (f,g))) = the carrier of (S with-replacement (f,g)) & dom (id the carrier' of (S with-replacement (f,g))) = the carrier' of (S with-replacement (f,g)) ) ; :: according to PUA2MSS1:def 12,INSTALG1:def 2 :: thesis:
dom g = the carrier' of S by A3;
then A7: the carrier' of S -indexing g = g by Th10;
A8: the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) by A5, Def4;

A9: now :: thesis:

let x be object ; :: thesis:
assume A10: x in the carrier' of (S with-replacement (f,g)) ; :: thesis:
then consider a being object such that
A11: a in dom g and
A12: x = g . a by A6, A7, FUNCT_1:def 3;
reconsider a = a as OperSymbol of S by A3, A11;
the ResultSort of (S with-replacement (f,g)) * g = f * the ResultSort of S by A8, A4, A7;
then A13: the ResultSort of (S with-replacement (f,g)) . x = (f * the ResultSort of S) . a by A11, A12, FUNCT_1:13;
the ResultSort of S9 * g = f * the ResultSort of S by A3;
then the ResultSort of S9 . x = (f * the ResultSort of S) . a by A11, A12, FUNCT_1:13;
hence the ResultSort of (S with-replacement (f,g)) . x = ( the ResultSort of S9 | the carrier' of (S with-replacement (f,g))) . x by A10, A13, FUNCT_1:49; :: thesis:

end;

rng g c= the carrier' of S9 by A3;
then dom ( the ResultSort of S9 | the carrier' of (S with-replacement (f,g))) = the carrier' of (S with-replacement (f,g)) by A6, A7, A1, RELAT_1:62;
then A14: the ResultSort of (S with-replacement (f,g)) = the ResultSort of S9 | the carrier' of (S with-replacement (f,g)) by A2, A9;
the carrier of (S with-replacement (f,g)) = rng ( the carrier of S -indexing f) by A5, Def4;
hence ( rng (id the carrier of (S with-replacement (f,g))) c= the carrier of S9 & rng (id the carrier' of (S with-replacement (f,g))) c= the carrier' of S9 ) by A3, A6, A4, A7; :: thesis:
rng the ResultSort of (S with-replacement (f,g)) c= the carrier of (S with-replacement (f,g)) ;
hence (id the carrier of (S with-replacement (f,g))) * the ResultSort of (S with-replacement (f,g)) = the ResultSort of (S with-replacement (f,g)) by RELAT_1:53
.= the ResultSort of S9 * (id the carrier' of (S with-replacement (f,g))) by A14, RELAT_1:65 ;
:: thesis:
let o be set ; :: thesis:
let p be Function; :: thesis:
assume that
A15: o in the carrier' of (S with-replacement (f,g)) and
A16: p = the Arity of (S with-replacement (f,g)) . o ; :: thesis:
consider a being object such that
A17: a in dom g and
A18: o = g . a by A6, A7, A15, FUNCT_1:def 3;
reconsider a = a as OperSymbol of S by A3, A17;
A19: f * (the_arity_of a) = the Arity of S9 . o by A3, A18;
p in the carrier of (S with-replacement (f,g)) * by A15, A16, FUNCT_2:5;
then p is FinSequence of the carrier of (S with-replacement (f,g)) by FINSEQ_1:def 11;
then A20: rng p c= the carrier of (S with-replacement (f,g)) by FINSEQ_1:def 4;
f * (the_arity_of a) = p by A8, A4, A7, A16, A18;
hence (id the carrier of (S with-replacement (f,g))) * p = the Arity of S9 . o by A20, A19, RELAT_1:53
.= the Arity of S9 . ((id the carrier' of (S with-replacement (f,g))) . o) by A15, FUNCT_1:18 ;
:: thesis: