let x be bound_QC-variable; :: thesis: for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
@ ((CQCSub_All [S,x],xSQ) `2 ) = ((@ (RestrictSub x,(All x,(S `1 )),xSQ)) +* ((@ xSQ) | (RSub1 (All x,(S `1 ))))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ))
let S be Element of CQC-Sub-WFF ; :: thesis: for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
@ ((CQCSub_All [S,x],xSQ) `2 ) = ((@ (RestrictSub x,(All x,(S `1 )),xSQ)) +* ((@ xSQ) | (RSub1 (All x,(S `1 ))))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ))
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable implies @ ((CQCSub_All [S,x],xSQ) `2 ) = ((@ (RestrictSub x,(All x,(S `1 )),xSQ)) +* ((@ xSQ) | (RSub1 (All x,(S `1 ))))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ)) )
set S1 = CQCSub_All [S,x],xSQ;
assume A1: [S,x] is quantifiable ; :: thesis: @ ((CQCSub_All [S,x],xSQ) `2 ) = ((@ (RestrictSub x,(All x,(S `1 )),xSQ)) +* ((@ xSQ) | (RSub1 (All x,(S `1 ))))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ))
then CQCSub_All [S,x],xSQ = Sub_All [S,x],xSQ by Def6;
then A2: @ ((CQCSub_All [S,x],xSQ) `2 ) = @ xSQ by A1, Th27;
A3: @ (RestrictSub x,(All x,(S `1 )),xSQ) = (@ xSQ) \ (((@ xSQ) | (RSub1 (All x,(S `1 )))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ))) by Th87;
then reconsider F = (@ xSQ) \ (((@ xSQ) | (RSub1 (All x,(S `1 )))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ))) as PartFunc of bound_QC-variables ,bound_QC-variables ;
A4: (((@ xSQ) | (RSub1 (All x,(S `1 )))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ))) \/ F = (((@ xSQ) | (RSub1 (All x,(S `1 )))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ))) \/ (@ xSQ) by XBOOLE_1:39;
dom ((@ xSQ) | (RSub1 (All x,(S `1 )))) misses dom ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ)) by Th86;
then A5: ((@ xSQ) | (RSub1 (All x,(S `1 )))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ)) = ((@ xSQ) | (RSub1 (All x,(S `1 )))) \/ ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ)) by FUNCT_4:32;
( (@ xSQ) | (RSub1 (All x,(S `1 ))) c= @ xSQ & (@ xSQ) | (RSub2 (All x,(S `1 )),xSQ) c= @ xSQ ) by RELAT_1:88;
then A6: (((@ xSQ) | (RSub1 (All x,(S `1 )))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ))) \/ F = @ xSQ by A4, A5, XBOOLE_1:8, XBOOLE_1:12;
dom F misses (dom ((@ xSQ) | (RSub1 (All x,(S `1 ))))) \/ (dom ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ))) by A3, Th88;
then dom F misses dom (((@ xSQ) | (RSub1 (All x,(S `1 )))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ))) by FUNCT_4:def 1;
then F +* (((@ xSQ) | (RSub1 (All x,(S `1 )))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ))) = @ xSQ by A6, FUNCT_4:32;
hence @ ((CQCSub_All [S,x],xSQ) `2 ) = ((@ (RestrictSub x,(All x,(S `1 )),xSQ)) +* ((@ xSQ) | (RSub1 (All x,(S `1 ))))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ)) by A2, A3, FUNCT_4:15; :: thesis: verum