A1: (QScope (p,x,Sub)) `1 = [p,((CFQ Al) . [(All (x,p)),Sub])] by MCART_1:7;
then ((QScope (p,x,Sub)) `1) `2 = ((QSub Al) | (CQC-Sub-WFF Al)) . [(All (x,p)),Sub] by MCART_1:7;
then A2: ((QScope (p,x,Sub)) `1) `2 = (QSub Al) . [(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