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;
A1: (@ xSQ) | (RSub2 (All x,(S `1 )),xSQ) c= @ xSQ by RELAT_1:88;
dom ((@ xSQ) | (RSub1 (All x,(S `1 )))) misses dom ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ)) by Th86;
then A2: ((@ 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;
assume A3: [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 A4: @ ((CQCSub_All [S,x],xSQ) `2 ) = @ xSQ by A3, Th27;
A5: @ (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 ;
dom F misses (dom ((@ xSQ) | (RSub1 (All x,(S `1 ))))) \/ (dom ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ))) by A5, Th88;
then A6: dom F misses dom (((@ xSQ) | (RSub1 (All x,(S `1 )))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ))) by FUNCT_4:def 1;
( (((@ 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) & (@ xSQ) | (RSub1 (All x,(S `1 ))) c= @ xSQ ) by RELAT_1:88, XBOOLE_1:39;
then (((@ xSQ) | (RSub1 (All x,(S `1 )))) +* ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ))) \/ F = @ xSQ by A2, A1, XBOOLE_1:8, XBOOLE_1:12;
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 A4, A5, FUNCT_4:15; :: thesis: verum