consider F being Function of CQC-WFF ,F₁() such that
A2: ( F . VERUM = F₃() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for l being CQC-variable_list of
for P being QC-pred_symbol of k holds
( F . (P ! l) = F₄(k,P,l) & F . ('not' r) = F₅((F . r)) & F . (r '&' s) = F₆((F . r),(F . s)) & F . (All x,r) = F₉(x,(F . r)) ) ) ) from CQC_LANG:sch 2();
A3: F . (F₇() '&' F₈()) = F₆((F . F₇()),(F . F₈())) by A2;
consider F1 being Function of CQC-WFF ,F₁() such that
A4: F₂(F₇()) = F1 . F₇() and
A5: ( F1 . VERUM = F₃() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for l being CQC-variable_list of
for P being QC-pred_symbol of k holds
( F1 . (P ! l) = F₄(k,P,l) & F1 . ('not' r) = F₅((F1 . r)) & F1 . (r '&' s) = F₆((F1 . r),(F1 . s)) & F1 . (All x,r) = F₉(x,(F1 . r)) ) ) ) by A1;
consider F2 being Function of CQC-WFF ,F₁() such that
A6: F₂(F₈()) = F2 . F₈() and
A7: ( F2 . VERUM = F₃() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for l being CQC-variable_list of
for P being QC-pred_symbol of k holds
( F2 . (P ! l) = F₄(k,P,l) & F2 . ('not' r) = F₅((F2 . r)) & F2 . (r '&' s) = F₆((F2 . r),(F2 . s)) & F2 . (All x,r) = F₉(x,(F2 . r)) ) ) ) by A1;
A8: F = F1 from CQC_LANG:sch 3(A2, A5);
F = F2 from CQC_LANG:sch 3(A2, A7);
hence F₂((F₇() '&' F₈())) = F₆(F₂(F₇()),F₂(F₈())) by A1, A2, A3, A4, A6, A8; :: thesis: verum