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 holds

( [(All (x,p)),Sub] = CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) & QScope (p,x,Sub) is quantifiable )

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

for Sub being CQC_Substitution of Al 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 of Al; :: thesis: for Sub being CQC_Substitution of Al 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 of Al; :: 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 Al) . [(All (x,p)),Sub])];

set B = [[p,((CFQ Al) . [(All (x,p)),Sub])],x];

A1: ( [[p,((CFQ Al) . [(All (x,p)),Sub])],x] `2 = x & ([[p,((CFQ Al) . [(All (x,p)),Sub])],x] `1) `1 = p ) ;

[(All (x,p)),Sub] in CQC-Sub-WFF Al ;

then A2: [(All (x,p)),Sub] in dom (CFQ Al) by FUNCT_2:def 1;

([[p,((CFQ Al) . [(All (x,p)),Sub])],x] `1) `2 = (QSub Al) . [(All (([[p,((CFQ Al) . [(All (x,p)),Sub])],x] `2),(([[p,((CFQ Al) . [(All (x,p)),Sub])],x] `1) `1))),Sub] by A2, FUNCT_1:47;

then A3: [[p,((CFQ Al) . [(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 5;

hence ( [(All (x,p)),Sub] = CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) & QScope (p,x,Sub) is quantifiable ) by A1, A3, SUBSTUT1:def 24; :: thesis: verum

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al holds

( [(All (x,p)),Sub] = CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) & QScope (p,x,Sub) is quantifiable )

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

for Sub being CQC_Substitution of Al 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 of Al; :: thesis: for Sub being CQC_Substitution of Al 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 of Al; :: 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 Al) . [(All (x,p)),Sub])];

set B = [[p,((CFQ Al) . [(All (x,p)),Sub])],x];

A1: ( [[p,((CFQ Al) . [(All (x,p)),Sub])],x] `2 = x & ([[p,((CFQ Al) . [(All (x,p)),Sub])],x] `1) `1 = p ) ;

[(All (x,p)),Sub] in CQC-Sub-WFF Al ;

then A2: [(All (x,p)),Sub] in dom (CFQ Al) by FUNCT_2:def 1;

([[p,((CFQ Al) . [(All (x,p)),Sub])],x] `1) `2 = (QSub Al) . [(All (([[p,((CFQ Al) . [(All (x,p)),Sub])],x] `2),(([[p,((CFQ Al) . [(All (x,p)),Sub])],x] `1) `1))),Sub] by A2, FUNCT_1:47;

then A3: [[p,((CFQ Al) . [(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 5;

hence ( [(All (x,p)),Sub] = CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) & QScope (p,x,Sub) is quantifiable ) by A1, A3, SUBSTUT1:def 24; :: thesis: verum