consider F2 being Function of (CQC-WFF F₁()),F₂() such that
A2: F₃(F₉()) = F2 . F₉() and
A3: ( F2 . (VERUM F₁()) = F₄() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() 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;
consider F1 being Function of (CQC-WFF F₁()),F₂() such that
A4: F₃(F₈()) = F1 . F₈() and
A5: ( F1 . (VERUM F₁()) = F₄() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() 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 F being Function of (CQC-WFF F₁()),F₂() such that
A6: ( F . (VERUM F₁()) = F₄() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() 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();
A7: F . (F₈() '&' F₉()) = F₇((F . F₈()),(F . F₉())) by A6;
A8: F = F2 from CQC_LANG:sch 3(A6, A3);
F = F1 from CQC_LANG:sch 3(A6, A5);
hence F₃((F₈() '&' F₉())) = F₇(F₃(F₈()),F₃(F₉())) by A1, A6, A7, A4, A2, A8; :: thesis: verum