let Al be QC-alphabet ; :: thesis: for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
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 x be bound_QC-variable of Al; :: thesis: for S being Element of CQC-Sub-WFF Al
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 Al; :: 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:59;
dom ((@ xSQ) | (RSub1 (All (x,(S `1))))) misses dom ((@ xSQ) | (RSub2 ((All (x,(S `1))),xSQ))) by Th82;
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:31;
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 Def5;
then A4: @ ((CQCSub_All ([S,x],xSQ)) `2) = @ xSQ by A3, Th26;
A5: @ (RestrictSub (x,(All (x,(S `1))),xSQ)) = (@ xSQ) \ (((@ xSQ) | (RSub1 (All (x,(S `1))))) +* ((@ xSQ) | (RSub2 ((All (x,(S `1))),xSQ)))) by Th83;
then reconsider F = (@ xSQ) \ (((@ xSQ) | (RSub1 (All (x,(S `1))))) +* ((@ xSQ) | (RSub2 ((All (x,(S `1))),xSQ)))) as PartFunc of (bound_QC-variables Al),(bound_QC-variables Al) ;
dom F misses (dom ((@ xSQ) | (RSub1 (All (x,(S `1)))))) \/ (dom ((@ xSQ) | (RSub2 ((All (x,(S `1))),xSQ)))) by A5, Th84;
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:59, 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:31;
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:14; :: thesis: verum