consider G being Function of (CQC-WFF F₁()),F₂() such that
A2: F₃(F₁₀()) = G . F₁₀() and
A3: ( G . (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
( 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₁()),F₂() such that
A4: ( 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();
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