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 k
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();
F₄(F₅(),F₆(),F₇()) = F . (F₆() ! F₇()) by A2;
hence F₃((F₆() ! F₇())) = F₄(F₅(),F₆(),F₇()) by A1, A2; :: thesis: verum