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; :: thesis: verum

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; :: thesis: verum