let Al be QC-alphabet ; :: thesis: for Al2 being Al -expanding QC-alphabet
for p2 being Element of CQC-WFF Al2
for S being CQC_Substitution of Al
for S2 being CQC_Substitution of Al2
for x2 being bound_QC-variable of Al2
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al st p = p2 & S = S2 & x = x2 holds
RestrictSub (x,p,S) = RestrictSub (x2,p2,S2)
let Al2 be Al -expanding QC-alphabet ; :: thesis: for p2 being Element of CQC-WFF Al2
for S being CQC_Substitution of Al
for S2 being CQC_Substitution of Al2
for x2 being bound_QC-variable of Al2
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al st p = p2 & S = S2 & x = x2 holds
RestrictSub (x,p,S) = RestrictSub (x2,p2,S2)
let p2 be Element of CQC-WFF Al2; :: thesis: for S being CQC_Substitution of Al
for S2 being CQC_Substitution of Al2
for x2 being bound_QC-variable of Al2
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al st p = p2 & S = S2 & x = x2 holds
RestrictSub (x,p,S) = RestrictSub (x2,p2,S2)
let S be CQC_Substitution of Al; :: thesis: for S2 being CQC_Substitution of Al2
for x2 being bound_QC-variable of Al2
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al st p = p2 & S = S2 & x = x2 holds
RestrictSub (x,p,S) = RestrictSub (x2,p2,S2)
let S2 be CQC_Substitution of Al2; :: thesis: for x2 being bound_QC-variable of Al2
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al st p = p2 & S = S2 & x = x2 holds
RestrictSub (x,p,S) = RestrictSub (x2,p2,S2)
let x2 be bound_QC-variable of Al2; :: thesis: for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al st p = p2 & S = S2 & x = x2 holds
RestrictSub (x,p,S) = RestrictSub (x2,p2,S2)
let x be bound_QC-variable of Al; :: thesis: for p being Element of CQC-WFF Al st p = p2 & S = S2 & x = x2 holds
RestrictSub (x,p,S) = RestrictSub (x2,p2,S2)
let p be Element of CQC-WFF Al; :: thesis: ( p = p2 & S = S2 & x = x2 implies RestrictSub (x,p,S) = RestrictSub (x2,p2,S2) )
assume A1: ( p = p2 & S = S2 & x = x2 ) ; :: thesis: RestrictSub (x,p,S) = RestrictSub (x2,p2,S2)
set rset = { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) } ;
set rset2 = { y2 where y2 is bound_QC-variable of Al2 : ( y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) } ;
{ y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) } = { y2 where y2 is bound_QC-variable of Al2 : ( y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) }

proof

for s being object st s in { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) } holds
s in { y2 where y2 is bound_QC-variable of Al2 : ( y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) }

proof

let s be object ; :: thesis: ( s in { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) } implies s in { y2 where y2 is bound_QC-variable of Al2 : ( y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) } )
assume A2: s in { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) } ; :: thesis: s in { y2 where y2 is bound_QC-variable of Al2 : ( y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) }
consider y being bound_QC-variable of Al such that
A3: ( s = y & y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) by A2;
reconsider y = y as bound_QC-variable of Al2 by Th4, TARSKI:def 3;
p2 = Al2 -Cast p by A1;
then ( y in still_not-bound_in p2 & y is Element of dom S2 & y <> x2 & y <> S2 . y ) by A1, A3, Th12;
hence s in { y2 where y2 is bound_QC-variable of Al2 : ( y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) } by A3; :: thesis: verum

end;

hence { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) } c= { y2 where y2 is bound_QC-variable of Al2 : ( y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) } ; :: according to XBOOLE_0:def 10 :: thesis: { y2 where y2 is bound_QC-variable of Al2 : ( y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) } c= { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) }
for s2 being object st s2 in { y2 where y2 is bound_QC-variable of Al2 : ( y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) } holds
s2 in { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) }

proof

let s2 be object ; :: thesis: ( s2 in { y2 where y2 is bound_QC-variable of Al2 : ( y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) } implies s2 in { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) } )
assume A4: s2 in { y2 where y2 is bound_QC-variable of Al2 : ( y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) } ; :: thesis: s2 in { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) }
consider y2 being bound_QC-variable of Al2 such that
A5: ( s2 = y2 & y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) by A4;
p2 = Al2 -Cast p by A1;
then A6: y2 in still_not-bound_in p by A5, Th12;
then reconsider y2 = y2 as bound_QC-variable of Al ;
thus s2 in { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) } by A1, A5, A6; :: thesis: verum

end;

hence { y2 where y2 is bound_QC-variable of Al2 : ( y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) } c= { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) } ; :: thesis: verum

end;

then ( S | { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) } = S2 | { y2 where y2 is bound_QC-variable of Al2 : ( y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) } & S | { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom S & y <> x & y <> S . y ) } = RestrictSub (x,p,S) & S2 | { y2 where y2 is bound_QC-variable of Al2 : ( y2 in still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2 . y2 ) } = RestrictSub (x2,p2,S2) ) by A1, SUBSTUT1:def 6;
hence RestrictSub (x,p,S) = RestrictSub (x2,p2,S2) ; :: thesis: verum