let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable
for Sub being CQC_Substitution holds
( [(All x,p),Sub] = CQCSub_All (QScope p,x,Sub),(Qsc p,x,Sub) & QScope p,x,Sub is quantifiable )
let x be bound_QC-variable; :: thesis: for Sub being CQC_Substitution holds
( [(All x,p),Sub] = CQCSub_All (QScope p,x,Sub),(Qsc p,x,Sub) & QScope p,x,Sub is quantifiable )
let Sub be CQC_Substitution; :: thesis: ( [(All x,p),Sub] = CQCSub_All (QScope p,x,Sub),(Qsc p,x,Sub) & QScope p,x,Sub is quantifiable )
set S = [p,(CFQ . [(All x,p),Sub])];
set B = [[p,(CFQ . [(All x,p),Sub])],x];
A1: [[p,(CFQ . [(All x,p),Sub])],x] `1 = [p,(CFQ . [(All x,p),Sub])] by MCART_1:7;
then A2: ( [[p,(CFQ . [(All x,p),Sub])],x] `2 = x & ([[p,(CFQ . [(All x,p),Sub])],x] `1 ) `1 = p ) by MCART_1:7;
[(All x,p),Sub] in CQC-Sub-WFF ;
then A3: [(All x,p),Sub] in dom CFQ by FUNCT_2:def 1;
([[p,(CFQ . [(All x,p),Sub])],x] `1 ) `2 = CFQ . [(All x,p),Sub] by A1, MCART_1:7;
then ([[p,(CFQ . [(All x,p),Sub])],x] `1 ) `2 = QSub . [(All ([[p,(CFQ . [(All x,p),Sub])],x] `2 ),(([[p,(CFQ . [(All x,p),Sub])],x] `1 ) `1 )),Sub] by A2, A3, FUNCT_1:70;
then A4: [[p,(CFQ . [(All x,p),Sub])],x] is quantifiable by SUBSTUT1:def 22;
then CQCSub_All (QScope p,x,Sub),(Qsc p,x,Sub) = Sub_All (QScope p,x,Sub),(Qsc p,x,Sub) by SUBLEMMA:def 6;
hence ( [(All x,p),Sub] = CQCSub_All (QScope p,x,Sub),(Qsc p,x,Sub) & QScope p,x,Sub is quantifiable ) by A2, A4, SUBSTUT1:def 24; :: thesis: verum