let f, g be Function; :: thesis: for S being non void Signature
for E being Extension of S st f,g form_a_replacement_in E holds
E with-replacement (f,g) is Extension of S with-replacement (f,g)
let S be non void Signature; :: thesis: for E being Extension of S st f,g form_a_replacement_in E holds
E with-replacement (f,g) is Extension of S with-replacement (f,g)
let E be Extension of S; :: thesis: ( f,g form_a_replacement_in E implies E with-replacement (f,g) is Extension of S with-replacement (f,g) )
set f9 = the carrier of E -indexing f;
set g9 = the carrier' of E -indexing g;
set gg = the carrier' of S -indexing g;
set T = E with-replacement (f,g);
A1: the carrier' of S -indexing ( the carrier' of S -indexing g) = the carrier' of S -indexing g by Th11;
assume A2: f,g form_a_replacement_in E ; :: thesis: E with-replacement (f,g) is Extension of S with-replacement (f,g)
then f,g form_a_replacement_in S by Th52;
then the carrier of S -indexing f, the carrier' of S -indexing g form_a_replacement_in S by Th30;
then A3: f, the carrier' of S -indexing g form_a_replacement_in S by A1, Th30;
A4: S is Subsignature of E by Def5;
then A5: ( the carrier' of E -indexing g) | the carrier' of S = the carrier' of S -indexing g by Th17, INSTALG1:10;
the carrier of E -indexing f, the carrier' of E -indexing g form_morphism_between E,E with-replacement (f,g) by A2, Th40;
then A6: S with-replacement ((( the carrier of E -indexing f) | the carrier of S),(( the carrier' of E -indexing g) | the carrier' of S)) is Subsignature of E with-replacement (f,g) by A4, Th39, INSTALG1:18;
( the carrier of E -indexing f) | the carrier of S = the carrier of S -indexing f by A4, Th17, INSTALG1:10;
then S with-replacement ((( the carrier of E -indexing f) | the carrier of S),(( the carrier' of E -indexing g) | the carrier' of S)) = S with-replacement (f,( the carrier' of S -indexing g)) by A3, A5, Th43;
hence S with-replacement (f,g) is Subsignature of E with-replacement (f,g) by A2, A6, Th44, Th52; :: according to ALGSPEC1:def 5 :: thesis: verum