consider G being Function of (CQC-WFF F1()),F2() such that
A2:
F3(F7()) = G . F7()
and
A3:
( G . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F5(k,P,l) & G . ('not' r) = F6((G . r)) & G . (r '&' s) = F8((G . r),(G . s)) & G . (All (x,r)) = F9(x,(G . r)) ) ) )
by A1;
consider F being Function of (CQC-WFF F1()),F2() such that
A4:
( F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F8((F . r),(F . s)) & F . (All (x,r)) = F9(x,(F . r)) ) ) )
from CQC_LANG:sch 2();
A5:
F . ('not' F7()) = F6((F . F7()))
by A4;
F = G
from CQC_LANG:sch 3(A4, A3);
hence
F3(('not' F7())) = F6(F3(F7()))
by A1, A4, A5, A2; verum