consider G being Function of CQC-WFF,F₁() such that
A2: F₂(F₉()) = G . F₉() and
A3: ( G . 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
( G . (P ! l) = F₄(k,P,l) & G . ('not' r) = F₅((G . r)) & G . (r '&' s) = F₆((G . r),(G . s)) & G . (All (x,r)) = F₇(x,(G . r)) ) ) ) by A1;
consider F being Function of CQC-WFF,F₁() such that
A4: ( 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();
A5: F . (All (F₈(),F₉())) = F₇(F₈(),(F . F₉())) by A4;
F = G from CQC_LANG:sch 3(A4, A3);
hence F₂((All (F₈(),F₉()))) = F₇(F₈(),F₂(F₉())) by A1, A4, A5, A2; :: thesis: verum