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