let Al be QC-alphabet ; :: thesis: for Al2 being Al -expanding QC-alphabet

for p2 being Element of CQC-WFF Al2

for S being finite CQC_Substitution of Al

for S2 being finite CQC_Substitution of Al2

for p being Element of CQC-WFF Al st S = S2 & p = p2 holds

upVar (S,p) = upVar (S2,p2)

let Al2 be Al -expanding QC-alphabet ; :: thesis: for p2 being Element of CQC-WFF Al2

for S being finite CQC_Substitution of Al

for S2 being finite CQC_Substitution of Al2

for p being Element of CQC-WFF Al st S = S2 & p = p2 holds

upVar (S,p) = upVar (S2,p2)

let p2 be Element of CQC-WFF Al2; :: thesis: for S being finite CQC_Substitution of Al

for S2 being finite CQC_Substitution of Al2

for p being Element of CQC-WFF Al st S = S2 & p = p2 holds

upVar (S,p) = upVar (S2,p2)

let S be finite CQC_Substitution of Al; :: thesis: for S2 being finite CQC_Substitution of Al2

for p being Element of CQC-WFF Al st S = S2 & p = p2 holds

upVar (S,p) = upVar (S2,p2)

let S2 be finite CQC_Substitution of Al2; :: thesis: for p being Element of CQC-WFF Al st S = S2 & p = p2 holds

upVar (S,p) = upVar (S2,p2)

let p be Element of CQC-WFF Al; :: thesis: ( S = S2 & p = p2 implies upVar (S,p) = upVar (S2,p2) )

assume A1: ( S = S2 & p = p2 ) ; :: thesis: upVar (S,p) = upVar (S2,p2)

A2: Sub_Var S = Sub_Var S2_{1}[ Element of QC-WFF Al] means for q2 being Element of CQC-WFF Al2 st $1 = q2 holds

Bound_Vars $1 = Bound_Vars q2;

A10: S_{1}[ VERUM Al]

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds S_{1}[P ! l]
_{1}[r] & S_{1}[s] holds

S_{1}[r '&' s]
_{1}[r] holds

S_{1}[ 'not' r]

for r being Element of CQC-WFF Al st S_{1}[r] holds

S_{1}[ All (x,r)]

for x being bound_QC-variable of Al

for k being Nat

for l being CQC-variable_list of k,Al

for P being QC-pred_symbol of k,Al holds

( S_{1}[ VERUM Al] & S_{1}[P ! l] & ( S_{1}[r] implies S_{1}[ 'not' r] ) & ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] ) & ( S_{1}[r] implies S_{1}[ All (x,r)] ) )
by A10, A12, A15, A21, A26;

A32: for q being Element of CQC-WFF Al holds S_{1}[q]
from CQC_LANG:sch 1(A31);

A33: Dom_Bound_Vars p = Dom_Bound_Vars p2

.= NSub (p2,S2) by A2, A33, SUBSTUT1:def 11 ;

thus upVar (S,p) = the Element of NSub (p,S) by SUBSTUT1:def 12

.= upVar (S2,p2) by A40, SUBSTUT1:def 12 ; :: thesis: verum

for p2 being Element of CQC-WFF Al2

for S being finite CQC_Substitution of Al

for S2 being finite CQC_Substitution of Al2

for p being Element of CQC-WFF Al st S = S2 & p = p2 holds

upVar (S,p) = upVar (S2,p2)

let Al2 be Al -expanding QC-alphabet ; :: thesis: for p2 being Element of CQC-WFF Al2

for S being finite CQC_Substitution of Al

for S2 being finite CQC_Substitution of Al2

for p being Element of CQC-WFF Al st S = S2 & p = p2 holds

upVar (S,p) = upVar (S2,p2)

let p2 be Element of CQC-WFF Al2; :: thesis: for S being finite CQC_Substitution of Al

for S2 being finite CQC_Substitution of Al2

for p being Element of CQC-WFF Al st S = S2 & p = p2 holds

upVar (S,p) = upVar (S2,p2)

let S be finite CQC_Substitution of Al; :: thesis: for S2 being finite CQC_Substitution of Al2

for p being Element of CQC-WFF Al st S = S2 & p = p2 holds

upVar (S,p) = upVar (S2,p2)

let S2 be finite CQC_Substitution of Al2; :: thesis: for p being Element of CQC-WFF Al st S = S2 & p = p2 holds

upVar (S,p) = upVar (S2,p2)

let p be Element of CQC-WFF Al; :: thesis: ( S = S2 & p = p2 implies upVar (S,p) = upVar (S2,p2) )

assume A1: ( S = S2 & p = p2 ) ; :: thesis: upVar (S,p) = upVar (S2,p2)

A2: Sub_Var S = Sub_Var S2

proof

defpred S
for s being object st s in Sub_Var S holds

s in Sub_Var S2

for s being object st s in Sub_Var S2 holds

s in Sub_Var S

end;s in Sub_Var S2

proof

hence
Sub_Var S c= Sub_Var S2
; :: according to XBOOLE_0:def 10 :: thesis: Sub_Var S2 c= Sub_Var S
let s be object ; :: thesis: ( s in Sub_Var S implies s in Sub_Var S2 )

assume A3: s in Sub_Var S ; :: thesis: s in Sub_Var S2

s in { t where t is QC-symbol of Al : x. t in rng S } by A3, SUBSTUT1:def 10;

then consider s2 being QC-symbol of Al such that

A4: ( s = s2 & x. s2 in rng S ) ;

( s2 in QC-symbols Al & QC-symbols Al c= QC-symbols Al2 ) by Th2;

then consider s3 being QC-symbol of Al2 such that

A5: s3 = s2 ;

x. s2 = [4,s2] by QC_LANG3:def 2

.= x. s3 by A5, QC_LANG3:def 2 ;

then s3 in { t where t is QC-symbol of Al2 : x. t in rng S2 } by A1, A4;

hence s in Sub_Var S2 by A4, A5, SUBSTUT1:def 10; :: thesis: verum

end;assume A3: s in Sub_Var S ; :: thesis: s in Sub_Var S2

s in { t where t is QC-symbol of Al : x. t in rng S } by A3, SUBSTUT1:def 10;

then consider s2 being QC-symbol of Al such that

A4: ( s = s2 & x. s2 in rng S ) ;

( s2 in QC-symbols Al & QC-symbols Al c= QC-symbols Al2 ) by Th2;

then consider s3 being QC-symbol of Al2 such that

A5: s3 = s2 ;

x. s2 = [4,s2] by QC_LANG3:def 2

.= x. s3 by A5, QC_LANG3:def 2 ;

then s3 in { t where t is QC-symbol of Al2 : x. t in rng S2 } by A1, A4;

hence s in Sub_Var S2 by A4, A5, SUBSTUT1:def 10; :: thesis: verum

for s being object st s in Sub_Var S2 holds

s in Sub_Var S

proof

hence
Sub_Var S2 c= Sub_Var S
; :: thesis: verum
let s be object ; :: thesis: ( s in Sub_Var S2 implies s in Sub_Var S )

assume A6: s in Sub_Var S2 ; :: thesis: s in Sub_Var S

s in { t where t is QC-symbol of Al2 : x. t in rng S2 } by A6, SUBSTUT1:def 10;

then consider s2 being QC-symbol of Al2 such that

A7: ( s = s2 & x. s2 in rng S2 ) ;

A8: rng (@ S) c= bound_QC-variables Al by SUBSTUT1:39;

x. s2 in rng (@ S) by A1, A7, SUBSTUT1:def 2;

then x. s2 in bound_QC-variables Al by A8;

then [4,s2] in [:{4},(QC-symbols Al):] by QC_LANG3:def 2;

then s2 in QC-symbols Al by ZFMISC_1:87;

then consider s3 being QC-symbol of Al such that

A9: s3 = s2 ;

x. s2 = [4,s2] by QC_LANG3:def 2

.= x. s3 by A9, QC_LANG3:def 2 ;

then s3 in { t where t is QC-symbol of Al : x. t in rng S } by A1, A7;

hence s in Sub_Var S by A7, A9, SUBSTUT1:def 10; :: thesis: verum

end;assume A6: s in Sub_Var S2 ; :: thesis: s in Sub_Var S

s in { t where t is QC-symbol of Al2 : x. t in rng S2 } by A6, SUBSTUT1:def 10;

then consider s2 being QC-symbol of Al2 such that

A7: ( s = s2 & x. s2 in rng S2 ) ;

A8: rng (@ S) c= bound_QC-variables Al by SUBSTUT1:39;

x. s2 in rng (@ S) by A1, A7, SUBSTUT1:def 2;

then x. s2 in bound_QC-variables Al by A8;

then [4,s2] in [:{4},(QC-symbols Al):] by QC_LANG3:def 2;

then s2 in QC-symbols Al by ZFMISC_1:87;

then consider s3 being QC-symbol of Al such that

A9: s3 = s2 ;

x. s2 = [4,s2] by QC_LANG3:def 2

.= x. s3 by A9, QC_LANG3:def 2 ;

then s3 in { t where t is QC-symbol of Al : x. t in rng S } by A1, A7;

hence s in Sub_Var S by A7, A9, SUBSTUT1:def 10; :: thesis: verum

Bound_Vars $1 = Bound_Vars q2;

A10: S

proof

A12:
for k being Nat
let q2 be Element of CQC-WFF Al2; :: thesis: ( VERUM Al = q2 implies Bound_Vars (VERUM Al) = Bound_Vars q2 )

assume A11: q2 = VERUM Al ; :: thesis: Bound_Vars (VERUM Al) = Bound_Vars q2

q2 = VERUM Al2 by A11;

hence Bound_Vars q2 = {} by SUBSTUT1:2

.= Bound_Vars (VERUM Al) by SUBSTUT1:2 ;

:: thesis: verum

end;assume A11: q2 = VERUM Al ; :: thesis: Bound_Vars (VERUM Al) = Bound_Vars q2

q2 = VERUM Al2 by A11;

hence Bound_Vars q2 = {} by SUBSTUT1:2

.= Bound_Vars (VERUM Al) by SUBSTUT1:2 ;

:: thesis: verum

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds S

proof

A15:
for r, s being Element of CQC-WFF Al st S
let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds S_{1}[P ! l]

let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S_{1}[P ! l]

let l be CQC-variable_list of k,Al; :: thesis: S_{1}[P ! l]

set P2 = Al2 -Cast P;

set l2 = Al2 -Cast l;

let q2 be Element of CQC-WFF Al2; :: thesis: ( P ! l = q2 implies Bound_Vars (P ! l) = Bound_Vars q2 )

assume A13: P ! l = q2 ; :: thesis: Bound_Vars (P ! l) = Bound_Vars q2

A14: q2 = Al2 -Cast (P ! l) by A13

.= (Al2 -Cast P) ! (Al2 -Cast l) by Th8 ;

thus Bound_Vars (P ! l) = still_not-bound_in (P ! l) by SUBLEMMA:43

.= still_not-bound_in (Al2 -Cast (P ! l)) by Th12

.= still_not-bound_in ((Al2 -Cast P) ! (Al2 -Cast l)) by Th8

.= Bound_Vars q2 by A14, SUBLEMMA:43 ; :: thesis: verum

end;for l being CQC-variable_list of k,Al holds S

let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S

let l be CQC-variable_list of k,Al; :: thesis: S

set P2 = Al2 -Cast P;

set l2 = Al2 -Cast l;

let q2 be Element of CQC-WFF Al2; :: thesis: ( P ! l = q2 implies Bound_Vars (P ! l) = Bound_Vars q2 )

assume A13: P ! l = q2 ; :: thesis: Bound_Vars (P ! l) = Bound_Vars q2

A14: q2 = Al2 -Cast (P ! l) by A13

.= (Al2 -Cast P) ! (Al2 -Cast l) by Th8 ;

thus Bound_Vars (P ! l) = still_not-bound_in (P ! l) by SUBLEMMA:43

.= still_not-bound_in (Al2 -Cast (P ! l)) by Th12

.= still_not-bound_in ((Al2 -Cast P) ! (Al2 -Cast l)) by Th8

.= Bound_Vars q2 by A14, SUBLEMMA:43 ; :: thesis: verum

S

proof

A21:
for r being Element of CQC-WFF Al st S
let r, s be Element of CQC-WFF Al; :: thesis: ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] )

assume A16: ( S_{1}[r] & S_{1}[s] )
; :: thesis: S_{1}[r '&' s]

set q = r '&' s;

set r2 = Al2 -Cast r;

set s2 = Al2 -Cast s;

let q2 be Element of CQC-WFF Al2; :: thesis: ( r '&' s = q2 implies Bound_Vars (r '&' s) = Bound_Vars q2 )

assume A17: r '&' s = q2 ; :: thesis: Bound_Vars (r '&' s) = Bound_Vars q2

A18: q2 = (Al2 -Cast r) '&' (Al2 -Cast s) by A17;

then ( r '&' s is conjunctive & q2 is conjunctive ) ;

then A19: ( the_left_argument_of (r '&' s) = r & the_right_argument_of (r '&' s) = s & the_left_argument_of q2 = Al2 -Cast r & the_right_argument_of q2 = Al2 -Cast s ) by A18, QC_LANG1:def 25, QC_LANG1:def 26;

A20: ( Bound_Vars r = Bound_Vars (Al2 -Cast r) & Bound_Vars s = Bound_Vars (Al2 -Cast s) ) by A16;

thus Bound_Vars (r '&' s) = (Bound_Vars r) \/ (Bound_Vars s) by A19, SUBSTUT1:5, QC_LANG1:def 20

.= Bound_Vars q2 by A18, A19, A20, SUBSTUT1:5, QC_LANG1:def 20 ; :: thesis: verum

end;assume A16: ( S

set q = r '&' s;

set r2 = Al2 -Cast r;

set s2 = Al2 -Cast s;

let q2 be Element of CQC-WFF Al2; :: thesis: ( r '&' s = q2 implies Bound_Vars (r '&' s) = Bound_Vars q2 )

assume A17: r '&' s = q2 ; :: thesis: Bound_Vars (r '&' s) = Bound_Vars q2

A18: q2 = (Al2 -Cast r) '&' (Al2 -Cast s) by A17;

then ( r '&' s is conjunctive & q2 is conjunctive ) ;

then A19: ( the_left_argument_of (r '&' s) = r & the_right_argument_of (r '&' s) = s & the_left_argument_of q2 = Al2 -Cast r & the_right_argument_of q2 = Al2 -Cast s ) by A18, QC_LANG1:def 25, QC_LANG1:def 26;

A20: ( Bound_Vars r = Bound_Vars (Al2 -Cast r) & Bound_Vars s = Bound_Vars (Al2 -Cast s) ) by A16;

thus Bound_Vars (r '&' s) = (Bound_Vars r) \/ (Bound_Vars s) by A19, SUBSTUT1:5, QC_LANG1:def 20

.= Bound_Vars q2 by A18, A19, A20, SUBSTUT1:5, QC_LANG1:def 20 ; :: thesis: verum

S

proof

A26:
for x being bound_QC-variable of Al
let r be Element of CQC-WFF Al; :: thesis: ( S_{1}[r] implies S_{1}[ 'not' r] )

assume A22: S_{1}[r]
; :: thesis: S_{1}[ 'not' r]

set q = 'not' r;

set r2 = Al2 -Cast r;

let q2 be Element of CQC-WFF Al2; :: thesis: ( 'not' r = q2 implies Bound_Vars ('not' r) = Bound_Vars q2 )

assume A23: 'not' r = q2 ; :: thesis: Bound_Vars ('not' r) = Bound_Vars q2

A24: q2 = 'not' (Al2 -Cast r) by A23;

then ( 'not' r is negative & q2 is negative ) ;

then A25: ( the_argument_of ('not' r) = r & the_argument_of q2 = Al2 -Cast r ) by A24, QC_LANG1:def 24;

thus Bound_Vars ('not' r) = Bound_Vars r by A25, SUBSTUT1:4, QC_LANG1:def 19

.= Bound_Vars (Al2 -Cast r) by A22

.= Bound_Vars q2 by A24, A25, SUBSTUT1:4, QC_LANG1:def 19 ; :: thesis: verum

end;assume A22: S

set q = 'not' r;

set r2 = Al2 -Cast r;

let q2 be Element of CQC-WFF Al2; :: thesis: ( 'not' r = q2 implies Bound_Vars ('not' r) = Bound_Vars q2 )

assume A23: 'not' r = q2 ; :: thesis: Bound_Vars ('not' r) = Bound_Vars q2

A24: q2 = 'not' (Al2 -Cast r) by A23;

then ( 'not' r is negative & q2 is negative ) ;

then A25: ( the_argument_of ('not' r) = r & the_argument_of q2 = Al2 -Cast r ) by A24, QC_LANG1:def 24;

thus Bound_Vars ('not' r) = Bound_Vars r by A25, SUBSTUT1:4, QC_LANG1:def 19

.= Bound_Vars (Al2 -Cast r) by A22

.= Bound_Vars q2 by A24, A25, SUBSTUT1:4, QC_LANG1:def 19 ; :: thesis: verum

for r being Element of CQC-WFF Al st S

S

proof

A31:
for r, s being Element of CQC-WFF Al
let x be bound_QC-variable of Al; :: thesis: for r being Element of CQC-WFF Al st S_{1}[r] holds

S_{1}[ All (x,r)]

let r be Element of CQC-WFF Al; :: thesis: ( S_{1}[r] implies S_{1}[ All (x,r)] )

assume A27: S_{1}[r]
; :: thesis: S_{1}[ All (x,r)]

set q = All (x,r);

set r2 = Al2 -Cast r;

set x2 = Al2 -Cast x;

let q2 be Element of CQC-WFF Al2; :: thesis: ( All (x,r) = q2 implies Bound_Vars (All (x,r)) = Bound_Vars q2 )

assume A28: All (x,r) = q2 ; :: thesis: Bound_Vars (All (x,r)) = Bound_Vars q2

A29: q2 = All ((Al2 -Cast x),(Al2 -Cast r)) by A28;

then ( All (x,r) is universal & q2 is universal ) ;

then A30: ( the_scope_of (All (x,r)) = r & bound_in (All (x,r)) = x & the_scope_of q2 = Al2 -Cast r & bound_in q2 = Al2 -Cast x ) by A29, QC_LANG1:def 27, QC_LANG1:def 28;

thus Bound_Vars (All (x,r)) = (Bound_Vars r) \/ {x} by A30, SUBSTUT1:6, QC_LANG1:def 21

.= (Bound_Vars (Al2 -Cast r)) \/ {(Al2 -Cast x)} by A27

.= Bound_Vars q2 by A29, A30, SUBSTUT1:6, QC_LANG1:def 21 ; :: thesis: verum

end;S

let r be Element of CQC-WFF Al; :: thesis: ( S

assume A27: S

set q = All (x,r);

set r2 = Al2 -Cast r;

set x2 = Al2 -Cast x;

let q2 be Element of CQC-WFF Al2; :: thesis: ( All (x,r) = q2 implies Bound_Vars (All (x,r)) = Bound_Vars q2 )

assume A28: All (x,r) = q2 ; :: thesis: Bound_Vars (All (x,r)) = Bound_Vars q2

A29: q2 = All ((Al2 -Cast x),(Al2 -Cast r)) by A28;

then ( All (x,r) is universal & q2 is universal ) ;

then A30: ( the_scope_of (All (x,r)) = r & bound_in (All (x,r)) = x & the_scope_of q2 = Al2 -Cast r & bound_in q2 = Al2 -Cast x ) by A29, QC_LANG1:def 27, QC_LANG1:def 28;

thus Bound_Vars (All (x,r)) = (Bound_Vars r) \/ {x} by A30, SUBSTUT1:6, QC_LANG1:def 21

.= (Bound_Vars (Al2 -Cast r)) \/ {(Al2 -Cast x)} by A27

.= Bound_Vars q2 by A29, A30, SUBSTUT1:6, QC_LANG1:def 21 ; :: thesis: verum

for x being bound_QC-variable of Al

for k being Nat

for l being CQC-variable_list of k,Al

for P being QC-pred_symbol of k,Al holds

( S

A32: for q being Element of CQC-WFF Al holds S

A33: Dom_Bound_Vars p = Dom_Bound_Vars p2

proof

A40: NSub (p,S) =
NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var S))
by SUBSTUT1:def 11
for s being object st s in Dom_Bound_Vars p holds

s in Dom_Bound_Vars p2

for s being object st s in Dom_Bound_Vars p2 holds

s in Dom_Bound_Vars p

end;s in Dom_Bound_Vars p2

proof

hence
Dom_Bound_Vars p c= Dom_Bound_Vars p2
; :: according to XBOOLE_0:def 10 :: thesis: Dom_Bound_Vars p2 c= Dom_Bound_Vars p
let s be object ; :: thesis: ( s in Dom_Bound_Vars p implies s in Dom_Bound_Vars p2 )

assume A34: s in Dom_Bound_Vars p ; :: thesis: s in Dom_Bound_Vars p2

s in { b where b is QC-symbol of Al : x. b in Bound_Vars p } by A34, SUBSTUT1:def 9;

then consider s2 being QC-symbol of Al such that

A35: ( s = s2 & x. s2 in Bound_Vars p ) ;

x. s2 in Bound_Vars p2 by A1, A32, A35;

then x. s2 in bound_QC-variables Al2 ;

then [4,s2] in [:{4},(QC-symbols Al2):] by QC_LANG3:def 2;

then s2 in QC-symbols Al2 by ZFMISC_1:87;

then consider s3 being QC-symbol of Al2 such that

A36: s3 = s2 ;

x. s2 = [4,s2] by QC_LANG3:def 2

.= x. s3 by A36, QC_LANG3:def 2 ;

then x. s3 in Bound_Vars p2 by A1, A32, A35;

then s3 in { b where b is QC-symbol of Al2 : x. b in Bound_Vars p2 } ;

hence s in Dom_Bound_Vars p2 by A35, A36, SUBSTUT1:def 9; :: thesis: verum

end;assume A34: s in Dom_Bound_Vars p ; :: thesis: s in Dom_Bound_Vars p2

s in { b where b is QC-symbol of Al : x. b in Bound_Vars p } by A34, SUBSTUT1:def 9;

then consider s2 being QC-symbol of Al such that

A35: ( s = s2 & x. s2 in Bound_Vars p ) ;

x. s2 in Bound_Vars p2 by A1, A32, A35;

then x. s2 in bound_QC-variables Al2 ;

then [4,s2] in [:{4},(QC-symbols Al2):] by QC_LANG3:def 2;

then s2 in QC-symbols Al2 by ZFMISC_1:87;

then consider s3 being QC-symbol of Al2 such that

A36: s3 = s2 ;

x. s2 = [4,s2] by QC_LANG3:def 2

.= x. s3 by A36, QC_LANG3:def 2 ;

then x. s3 in Bound_Vars p2 by A1, A32, A35;

then s3 in { b where b is QC-symbol of Al2 : x. b in Bound_Vars p2 } ;

hence s in Dom_Bound_Vars p2 by A35, A36, SUBSTUT1:def 9; :: thesis: verum

for s being object st s in Dom_Bound_Vars p2 holds

s in Dom_Bound_Vars p

proof

hence
Dom_Bound_Vars p2 c= Dom_Bound_Vars p
; :: thesis: verum
let s be object ; :: thesis: ( s in Dom_Bound_Vars p2 implies s in Dom_Bound_Vars p )

assume A37: s in Dom_Bound_Vars p2 ; :: thesis: s in Dom_Bound_Vars p

s in { b where b is QC-symbol of Al2 : x. b in Bound_Vars p2 } by A37, SUBSTUT1:def 9;

then consider s2 being QC-symbol of Al2 such that

A38: ( s = s2 & x. s2 in Bound_Vars p2 ) ;

x. s2 in Bound_Vars p by A1, A32, A38;

then x. s2 in bound_QC-variables Al ;

then [4,s2] in [:{4},(QC-symbols Al):] by QC_LANG3:def 2;

then s2 in QC-symbols Al by ZFMISC_1:87;

then consider s3 being QC-symbol of Al such that

A39: s3 = s2 ;

x. s2 = [4,s2] by QC_LANG3:def 2

.= x. s3 by A39, QC_LANG3:def 2 ;

then x. s3 in Bound_Vars p by A1, A32, A38;

then s3 in { b where b is QC-symbol of Al : x. b in Bound_Vars p } ;

hence s in Dom_Bound_Vars p by A38, A39, SUBSTUT1:def 9; :: thesis: verum

end;assume A37: s in Dom_Bound_Vars p2 ; :: thesis: s in Dom_Bound_Vars p

s in { b where b is QC-symbol of Al2 : x. b in Bound_Vars p2 } by A37, SUBSTUT1:def 9;

then consider s2 being QC-symbol of Al2 such that

A38: ( s = s2 & x. s2 in Bound_Vars p2 ) ;

x. s2 in Bound_Vars p by A1, A32, A38;

then x. s2 in bound_QC-variables Al ;

then [4,s2] in [:{4},(QC-symbols Al):] by QC_LANG3:def 2;

then s2 in QC-symbols Al by ZFMISC_1:87;

then consider s3 being QC-symbol of Al such that

A39: s3 = s2 ;

x. s2 = [4,s2] by QC_LANG3:def 2

.= x. s3 by A39, QC_LANG3:def 2 ;

then x. s3 in Bound_Vars p by A1, A32, A38;

then s3 in { b where b is QC-symbol of Al : x. b in Bound_Vars p } ;

hence s in Dom_Bound_Vars p by A38, A39, SUBSTUT1:def 9; :: thesis: verum

.= NSub (p2,S2) by A2, A33, SUBSTUT1:def 11 ;

thus upVar (S,p) = the Element of NSub (p,S) by SUBSTUT1:def 12

.= upVar (S2,p2) by A40, SUBSTUT1:def 12 ; :: thesis: verum