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:72;
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