consider F being Function of (CQC-WFF F1()),F2() such that
A2:
( F . (VERUM F1()) = F3() & ( 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) = F9((F . r)) & F . (r '&' s) = F10((F . r),(F . s)) & F . (All (x,r)) = F11(x,(F . r)) ) ) )
from CQC_LANG:sch 2();
F5(F6(),F7(),F8()) = F . (F7() ! F8())
by A2;
hence
F4((F7() ! F8())) = F5(F6(),F7(),F8())
by A1, A2; verum