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 . (All F₈(),F₉()) = F₇(F₈(),(F . F₉())) by A2;
consider G being Function of CQC-WFF ,F₁() such that
A4: F₂(F₉()) = G . F₉() and
A5: ( 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
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;
F = G from CQC_LANG:sch 3(A2, A5);
hence F₂((All F₈(),F₉())) = F₇(F₈(),F₂(F₉())) by A1, A2, A3, A4; :: thesis: verum