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

A11: 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 S9 | the carrier' of (S with-replacement f,g)) . x )
assume A12: x in the carrier' of (S with-replacement f,g) ; :: thesis: the ResultSort of (S with-replacement f,g) . x = (the ResultSort of S9 | the carrier' of (S with-replacement f,g)) . x
then consider a being set such that
A13: a in dom g and
A14: x = g . a by A7, A9, FUNCT_1:def 5;
reconsider a = a as OperSymbol of S by A4, A13, PUA2MSS1:def 13;
the ResultSort of (S with-replacement f,g) * g = f * the ResultSort of S by A10, A5, A9, PUA2MSS1:def 13;
then A15: the ResultSort of (S with-replacement f,g) . x = (f * the ResultSort of S) . a by A13, A14, FUNCT_1:23;
the ResultSort of S9 * g = f * the ResultSort of S by A4, PUA2MSS1:def 13;
then the ResultSort of S9 . x = (f * the ResultSort of S) . a by A13, A14, FUNCT_1:23;
hence the ResultSort of (S with-replacement f,g) . x = (the ResultSort of S9 | the carrier' of (S with-replacement f,g)) . x by A12, A15, FUNCT_1:72; :: thesis: verum

end;

rng g c= the carrier' of S9 by A4, PUA2MSS1:def 13;
then dom (the ResultSort of S9 | the carrier' of (S with-replacement f,g)) = the carrier' of (S with-replacement f,g) by A7, A9, A2, RELAT_1:91;
then A16: the ResultSort of (S with-replacement f,g) = the ResultSort of S9 | the carrier' of (S with-replacement f,g) by A3, A11, FUNCT_1:9;
the carrier of (S with-replacement f,g) = rng (the carrier of S -indexing f) by A6, 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 A4, A7, A5, A9, A1, A8, 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 S9 & ( 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 S9 . ((id the carrier' of (S with-replacement f,g)) . b₁) ) ) )
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:79
.= the ResultSort of S9 * (id the carrier' of (S with-replacement f,g)) by A16, 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 S9 . ((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 S9 . ((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 S9 . ((id the carrier' of (S with-replacement f,g)) . o) )
assume that
A17: o in the carrier' of (S with-replacement f,g) and
A18: p = the Arity of (S with-replacement f,g) . o ; :: thesis: p * (id the carrier of (S with-replacement f,g)) = the Arity of S9 . ((id the carrier' of (S with-replacement f,g)) . o)
consider a being set such that
A19: a in dom g and
A20: o = g . a by A7, A9, A17, FUNCT_1:def 5;
reconsider a = a as OperSymbol of S by A4, A19, PUA2MSS1:def 13;
A21: f * (the_arity_of a) = the Arity of S9 . o by A4, A20, PUA2MSS1:def 13;
p in the carrier of (S with-replacement f,g) * by A17, A18, FUNCT_2:7;
then p is FinSequence of the carrier of (S with-replacement f,g) by FINSEQ_1:def 11;
then A22: rng p c= the carrier of (S with-replacement f,g) by FINSEQ_1:def 4;
f * (the_arity_of a) = p by A10, A5, A9, A18, A20, PUA2MSS1:def 13;
hence (id the carrier of (S with-replacement f,g)) * p = the Arity of S9 . o by A22, A21, RELAT_1:79
.= the Arity of S9 . ((id the carrier' of (S with-replacement f,g)) . o) by A17, FUNCT_1:35 ;
:: thesis: verum