deffunc H5( Element of NAT , QC-pred_symbol of $1, CQC-variable_list of $1) -> Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF = ATOMIC $2,$3;
set D = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):];
deffunc H6( Function of [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF , set ) -> Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF = NEGATIVE $1;
deffunc H7( Function of [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF , Function of [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF , Element of CQC-WFF , set ) -> Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF = CON $1,$2,(QuantNbr $3);
deffunc H8( Element of bound_QC-variables , Function of [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF , set ) -> Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF = UNIVERSAL $1,$2;
reconsider V = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM as Function of [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF ;
reconsider V = V as Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF by FUNCT_2:11;
consider F being Function of CQC-WFF ,(Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF ) such that
A1:
F . VERUM = V
and
A2:
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) = H5(k,P,l)
and
A3:
for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( F . ('not' r) = H6(F . r,r) & F . (r '&' s) = H7(F . r,F . s,r,s) & F . (All x,r) = H8(x,F . r,r) )
from CQC_SIM1:sch 2();
take
F
; ( F . VERUM = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM & ( 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) = ATOMIC P,l ) & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( F . ('not' r) = NEGATIVE (F . r) & F . (r '&' s) = CON (F . r),(F . s),(QuantNbr r) & F . (All x,r) = UNIVERSAL x,(F . r) ) ) )
thus
( F . VERUM = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM & ( 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) = ATOMIC P,l ) & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( F . ('not' r) = NEGATIVE (F . r) & F . (r '&' s) = CON (F . r),(F . s),(QuantNbr r) & F . (All x,r) = UNIVERSAL x,(F . r) ) ) )
by A1, A2, A3; verum