let Al be QC-alphabet ; 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; 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; 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; ( [(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; verum