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 f' = the carrier of E -indexing f;
set g' = the carrier' of E -indexing g;
set gg = the carrier' of S -indexing g;
set T = E with-replacement f,g;
assume A1: 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 Th54;
then ( the carrier of S -indexing f,the carrier' of S -indexing g form_a_replacement_in S & the carrier' of S -indexing (the carrier' of S -indexing g) = the carrier' of S -indexing g ) by Th11, Th31;
then A2: f,the carrier' of S -indexing g form_a_replacement_in S by Th31;
A3: ( the carrier of E -indexing f,the carrier' of E -indexing g form_morphism_between E,E with-replacement f,g & S is Subsignature of E ) by A1, Def5, Th41;
then A4: 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 Th40, INSTALG1:19;
A5: (the carrier of E -indexing f) | the carrier of S = the carrier of S -indexing f by Th18, A3, INSTALG1:11;
(the carrier' of E -indexing g) | the carrier' of S = the carrier' of S -indexing g by Th18, A3, INSTALG1:11;
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 A2, A5, Th44;
hence S with-replacement f,g is Subsignature of E with-replacement f,g by A1, A4, Th45, Th54; :: according to ALGSPEC1:def 5 :: thesis: verum