A1:
((QScope (p,x,Sub)) `1) `2 = (QSub Al) . [(All (x,p)),Sub]
by FUNCT_1:49;
A2:
( (QScope (p,x,Sub)) `2 = x & ((QScope (p,x,Sub)) `1) `1 = p )
;
then
QScope (p,x,Sub) is quantifiable
by A1, SUBSTUT1:def 22;
hence
Sub is second_Q_comp of QScope (p,x,Sub)
by A2, A1, SUBSTUT1:def 23; verum