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
f,g form_a_replacement_in S
let S be non void Signature; :: thesis: for E being Extension of S st f,g form_a_replacement_in E holds
f,g form_a_replacement_in S
let E be Extension of S; :: thesis: ( f,g form_a_replacement_in E implies f,g form_a_replacement_in S )
set f9 = the carrier of E -indexing f;
set g9 = the carrier' of E -indexing g;
set T = E with-replacement (f,g);
A1: S is Subsignature of E by Def5;
then A2: ( the carrier of E -indexing f) | the carrier of S = the carrier of S -indexing f by Th17, INSTALG1:10;
A3: ( the carrier' of E -indexing g) | the carrier' of S = the carrier' of S -indexing g by A1, Th17, INSTALG1:10;
assume f,g form_a_replacement_in E ; :: thesis: f,g form_a_replacement_in S
then the carrier of E -indexing f, the carrier' of E -indexing g form_morphism_between E,E with-replacement (f,g) by Th40;
then ( the carrier of E -indexing f) | the carrier of S,( the carrier' of E -indexing g) | the carrier' of S form_a_replacement_in S by A1, Th31, INSTALG1:18;
hence f,g form_a_replacement_in S by A2, A3, Th30; :: thesis: verum