let S, S' be non void Signature; :: thesis: for f, g being Function st f,g form_morphism_between S,S' holds
S with-replacement f,g is Subsignature of S'
let f, g be Function; :: thesis: ( f,g form_morphism_between S,S' implies S with-replacement f,g is Subsignature of S' )
assume A1: f,g form_morphism_between S,S' ; :: thesis: S with-replacement f,g is Subsignature of S'
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 f' = the carrier of S -indexing f;
set g' = the carrier' of S -indexing g;
A2: f,g form_a_replacement_in S by A1, Th32;
then A3: the carrier of S -indexing f,the carrier' of S -indexing g form_morphism_between S,S with-replacement f,g by Def4;
A4: the carrier of (S with-replacement f,g) = rng (the carrier of S -indexing f) by A2, Def4;
A5: the carrier' of (S with-replacement f,g) = rng (the carrier' of S -indexing g) by A2, 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) ) by RELAT_1:71; :: according to PUA2MSS1:def 13,INSTALG1:def 2 :: thesis: ( rng (id the carrier of (S with-replacement f,g)) c= the carrier of S' & rng (id the carrier' of (S with-replacement f,g)) c= the carrier' of S' & the ResultSort of (S with-replacement f,g) * (id the carrier of (S with-replacement f,g)) = (id the carrier' of (S with-replacement f,g)) * the ResultSort of S' & ( for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of (S with-replacement f,g) or not b₂ = the Arity of (S with-replacement f,g) . b₁ or b₂ * (id the carrier of (S with-replacement f,g)) = the Arity of S' . ((id the carrier' of (S with-replacement f,g)) . b₁) ) ) )
( dom f = the carrier of S & dom g = the carrier' of S ) by A1, PUA2MSS1:def 13;
then A6: ( the carrier of S -indexing f = f & the carrier' of S -indexing g = g ) by Th10;
( rng (id the carrier of (S with-replacement f,g)) = the carrier of (S with-replacement f,g) & rng (id the carrier' of (S with-replacement f,g)) = the carrier' of (S with-replacement f,g) ) by RELAT_1:71;
hence ( rng (id the carrier of (S with-replacement f,g)) c= the carrier of S' & rng (id the carrier' of (S with-replacement f,g)) c= the carrier' of S' ) by A1, A4, A5, A6, PUA2MSS1:def 13; :: thesis: ( the ResultSort of (S with-replacement f,g) * (id the carrier of (S with-replacement f,g)) = (id the carrier' of (S with-replacement f,g)) * the ResultSort of S' & ( for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of (S with-replacement f,g) or not b₂ = the Arity of (S with-replacement f,g) . b₁ or b₂ * (id the carrier of (S with-replacement f,g)) = the Arity of S' . ((id the carrier' of (S with-replacement f,g)) . b₁) ) ) )
( rng g c= the carrier' of S' & dom the ResultSort of S' = the carrier' of S' ) by A1, FUNCT_2:def 1, PUA2MSS1:def 13;
then A7: dom (the ResultSort of S' | the carrier' of (S with-replacement f,g)) = the carrier' of (S with-replacement f,g) by A5, A6, RELAT_1:91;
A8: ( dom the ResultSort of (S with-replacement f,g) = the carrier' of (S with-replacement f,g) & rng the ResultSort of (S with-replacement f,g) c= the carrier of (S with-replacement f,g) ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in the carrier' of (S with-replacement f,g) implies the ResultSort of (S with-replacement f,g) . x = (the ResultSort of S' | the carrier' of (S with-replacement f,g)) . x )
assume A9: x in the carrier' of (S with-replacement f,g) ; :: thesis: the ResultSort of (S with-replacement f,g) . x = (the ResultSort of S' | the carrier' of (S with-replacement f,g)) . x
then consider a being set such that
A10: ( a in dom g & x = g . a ) by A5, A6, FUNCT_1:def 5;
reconsider a = a as OperSymbol of S by A1, A10, PUA2MSS1:def 13;
the ResultSort of S' * g = f * the ResultSort of S by A1, PUA2MSS1:def 13;
then A11: the ResultSort of S' . x = (f * the ResultSort of S) . a by A10, FUNCT_1:23;
the ResultSort of (S with-replacement f,g) * g = f * the ResultSort of S by A3, A6, PUA2MSS1:def 13;
then the ResultSort of (S with-replacement f,g) . x = (f * the ResultSort of S) . a by A10, FUNCT_1:23;
hence the ResultSort of (S with-replacement f,g) . x = (the ResultSort of S' | the carrier' of (S with-replacement f,g)) . x by A9, A11, FUNCT_1:72; :: thesis: verum

end;

then A12: the ResultSort of (S with-replacement f,g) = the ResultSort of S' | the carrier' of (S with-replacement f,g) by A7, A8, FUNCT_1:9;
thus (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 A8, RELAT_1:79
.= the ResultSort of S' * (id the carrier' of (S with-replacement f,g)) by A12, RELAT_1:94 ; :: thesis: for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of (S with-replacement f,g) or not b₂ = the Arity of (S with-replacement f,g) . b₁ or b₂ * (id the carrier of (S with-replacement f,g)) = the Arity of S' . ((id the carrier' of (S with-replacement f,g)) . b₁) )
let o be set ; :: thesis: for b₁ being set holds
( not o in the carrier' of (S with-replacement f,g) or not b₁ = the Arity of (S with-replacement f,g) . o or b₁ * (id the carrier of (S with-replacement f,g)) = the Arity of S' . ((id the carrier' of (S with-replacement f,g)) . o) )
let p be Function; :: thesis: ( not o in the carrier' of (S with-replacement f,g) or not p = the Arity of (S with-replacement f,g) . o or p * (id the carrier of (S with-replacement f,g)) = the Arity of S' . ((id the carrier' of (S with-replacement f,g)) . o) )
assume A13: ( o in the carrier' of (S with-replacement f,g) & p = the Arity of (S with-replacement f,g) . o ) ; :: thesis: p * (id the carrier of (S with-replacement f,g)) = the Arity of S' . ((id the carrier' of (S with-replacement f,g)) . o)
then consider a being set such that
A14: ( a in dom g & o = g . a ) by A5, A6, FUNCT_1:def 5;
p in the carrier of (S with-replacement f,g) * by A13, FUNCT_2:7;
then p is FinSequence of the carrier of (S with-replacement f,g) by FINSEQ_1:def 11;
then A15: rng p c= the carrier of (S with-replacement f,g) by FINSEQ_1:def 4;
reconsider a = a as OperSymbol of S by A1, A14, PUA2MSS1:def 13;
( f * (the_arity_of a) = p & f * (the_arity_of a) = the Arity of S' . o ) by A1, A3, A6, A13, A14, PUA2MSS1:def 13;
hence (id the carrier of (S with-replacement f,g)) * p = the Arity of S' . o by A15, RELAT_1:79
.= the Arity of S' . ((id the carrier' of (S with-replacement f,g)) . o) by A13, FUNCT_1:35 ;
:: thesis: verum