deffunc H5( Nat, QC-pred_symbol of $1,A, CQC-variable_list of $1,A) -> Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) = ATOMIC ($2,$3);
set D = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):];
deffunc H6( Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A), set ) -> Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) = NEGATIVE $1;
deffunc H7( Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A), Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A), Element of CQC-WFF A, set ) -> Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) = CON ($1,$2,(QuantNbr $3));
deffunc H8( Element of bound_QC-variables A, Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A), set ) -> Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) = UNIVERSAL ($1,$2);
reconsider V = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) as Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A) ;
let F, G be Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))); ( F . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Nat
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds F . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A 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)) ) ) & G . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Nat
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds G . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A holds
( G . ('not' r) = NEGATIVE (G . r) & G . (r '&' s) = CON ((G . r),(G . s),(QuantNbr r)) & G . (All (x,r)) = UNIVERSAL (x,(G . r)) ) ) implies F = G )
assume that
A4:
F . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A)
and
A5:
for k being Nat
for ll being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds F . (P ! ll) = H5(k,P,ll)
and
A6:
for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A 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) )
and
A7:
G . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A)
and
A8:
for k being Nat
for ll being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds G . (P ! ll) = H5(k,P,ll)
and
A9:
for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A holds
( G . ('not' r) = H6(G . r,r) & G . (r '&' s) = H7(G . r,G . s,r,s) & G . (All (x,r)) = H8(x,G . r,r) )
; F = G
A10:
G . (VERUM A) = V
by A7;
A11:
F . (VERUM A) = V
by A4;
thus
F = G
from CQC_SIM1:sch 3(A11, A5, A6, A10, A8, A9); verum