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