set D = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):];
deffunc H₅( Element of NAT , QC-pred_symbol of $1, CQC-variable_list of ) -> Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF = ATOMIC $2,$3;
deffunc H₆( 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 H₇( 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 H₈( 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 ;
let F, G be Function of CQC-WFF ,(Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF ); :: thesis: ( F . VERUM = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM & ( 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) = 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) ) ) & G . VERUM = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM & ( 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) = ATOMIC P,l ) & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables 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 = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM and
A5: for k being Element of NAT
for ll being CQC-variable_list of
for P being QC-pred_symbol of k holds F . (P ! ll) = H₅(k,P,ll) and
A6: for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( F . ('not' r) = H₆(F . r,r) & F . (r '&' s) = H₇(F . r,F . s,r,s) & F . (All x,r) = H₈(x,F . r,r) ) and
A7: G . VERUM = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM and
A8: for k being Element of NAT
for ll being CQC-variable_list of
for P being QC-pred_symbol of k holds G . (P ! ll) = H₅(k,P,ll) and
A9: for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( G . ('not' r) = H₆(G . r,r) & G . (r '&' s) = H₇(G . r,G . s,r,s) & G . (All x,r) = H₈(x,G . r,r) ) ; :: thesis: F = G
A10: F . VERUM = V by A4;
A11: G . VERUM = V by A7;
thus F = G from CQC_SIM1:sch 3(A10, A5, A6, A11, A8, A9); :: thesis: verum