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 ) }

hence RestrictSub (x,p,S) = RestrictSub (x2,p2,S2) ; :: thesis: verum

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

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;
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 ) }

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 ) }

end;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

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 ) }
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;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

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

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
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;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

hence RestrictSub (x,p,S) = RestrictSub (x2,p2,S2) ; :: thesis: verum