A1: (QScope (p,x,Sub)) `1 = [p,(CFQ . [(All (x,p)),Sub])] by MCART_1:7;
then ((QScope (p,x,Sub)) `1) `2 = (QSub | CQC-Sub-WFF) . [(All (x,p)),Sub] by MCART_1:7;
then A2: ((QScope (p,x,Sub)) `1) `2 = QSub . [(All (x,p)),Sub] by FUNCT_1:49;
A3: ( (QScope (p,x,Sub)) `2 = x & ((QScope (p,x,Sub)) `1) `1 = p ) by A1, MCART_1:7;
then QScope (p,x,Sub) is quantifiable by A2, SUBSTUT1:def 22;
hence Sub is second_Q_comp of QScope (p,x,Sub) by A3, A2, SUBSTUT1:def 23; :: thesis: verum