let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al

for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds

( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] )

let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al

for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds

( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] )

let x be bound_QC-variable of Al; :: thesis: for Sub being CQC_Substitution of Al

for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds

( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] )

let Sub be CQC_Substitution of Al; :: thesis: for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds

( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] )

let S be Element of CQC-Sub-WFF Al; :: thesis: ( S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p implies ( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] ) )

set Sub1 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub]));

reconsider Sub = Sub as CQC_Substitution of Al ;

assume that

A1: S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) and

A2: S `1 = p ; :: thesis: ( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] )

A3: ( [S,x] `2 = x & ([S,x] `1) `1 = p ) by A2;

A4: ( the_scope_of (All (x,p)) = p & All (x,p) is universal ) by QC_LANG1:def 21, QC_LANG2:7;

( (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) = ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) & bound_in (All (x,p)) = x ) by Th9, QC_LANG2:7;

then All (x,p),Sub PQSub (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A4, SUBSTUT1:def 14;

then consider a being object such that

A5: a = [[(All (x,p)),Sub],((@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])))] and

A6: All (x,p),Sub PQSub (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) ;

a in QSub Al by A5, A6, SUBSTUT1:def 15;

then A7: (QSub Al) . [(All (x,p)),Sub] = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A5, FUNCT_1:1;

A8: ([S,x] `1) `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A1;

hence [S,x] is quantifiable by A7, A3, SUBSTUT1:def 22; :: thesis: ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub]

A9: [S,x] is quantifiable by A7, A8, A3, SUBSTUT1:def 22;

then reconsider Sub = Sub as second_Q_comp of [S,x] by A7, A8, A3, SUBSTUT1:def 23;

take S1 = CQCSub_All ([S,x],Sub); :: thesis: S1 = [(All (x,p)),Sub]

S1 = Sub_All ([S,x],Sub) by A9, SUBLEMMA:def 5;

hence S1 = [(All (x,p)),Sub] by A3, A9, SUBSTUT1:def 24; :: thesis: verum

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al

for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds

( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] )

let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al

for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds

( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] )

let x be bound_QC-variable of Al; :: thesis: for Sub being CQC_Substitution of Al

for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds

( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] )

let Sub be CQC_Substitution of Al; :: thesis: for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds

( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] )

let S be Element of CQC-Sub-WFF Al; :: thesis: ( S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p implies ( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] ) )

set Sub1 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub]));

reconsider Sub = Sub as CQC_Substitution of Al ;

assume that

A1: S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) and

A2: S `1 = p ; :: thesis: ( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] )

A3: ( [S,x] `2 = x & ([S,x] `1) `1 = p ) by A2;

A4: ( the_scope_of (All (x,p)) = p & All (x,p) is universal ) by QC_LANG1:def 21, QC_LANG2:7;

( (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) = ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) & bound_in (All (x,p)) = x ) by Th9, QC_LANG2:7;

then All (x,p),Sub PQSub (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A4, SUBSTUT1:def 14;

then consider a being object such that

A5: a = [[(All (x,p)),Sub],((@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])))] and

A6: All (x,p),Sub PQSub (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) ;

a in QSub Al by A5, A6, SUBSTUT1:def 15;

then A7: (QSub Al) . [(All (x,p)),Sub] = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A5, FUNCT_1:1;

A8: ([S,x] `1) `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A1;

hence [S,x] is quantifiable by A7, A3, SUBSTUT1:def 22; :: thesis: ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub]

A9: [S,x] is quantifiable by A7, A8, A3, SUBSTUT1:def 22;

then reconsider Sub = Sub as second_Q_comp of [S,x] by A7, A8, A3, SUBSTUT1:def 23;

take S1 = CQCSub_All ([S,x],Sub); :: thesis: S1 = [(All (x,p)),Sub]

S1 = Sub_All ([S,x],Sub) by A9, SUBLEMMA:def 5;

hence S1 = [(All (x,p)),Sub] by A3, A9, SUBSTUT1:def 24; :: thesis: verum