let k be Element of NAT ; :: thesis: for ll being CQC-variable_list of
for P being QC-pred_symbol of k holds QuantNbr (P ! ll) = 0
let ll be CQC-variable_list of ; :: thesis: for P being QC-pred_symbol of k holds QuantNbr (P ! ll) = 0
let P be QC-pred_symbol of k; :: thesis: QuantNbr (P ! ll) = 0
A1: for p being Element of CQC-WFF
for d being Element of NAT holds
( d = H₅(p) iff ex F being Function of CQC-WFF ,NAT st
( d = F . p & F . VERUM = 0 & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables
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) = H₁(k,P,l) & F . ('not' r) = H₂(F . r) & F . (r '&' s) = H₃(F . r,F . s) & F . (All x,r) = H₄(x,F . r) ) ) ) ) by Def5;
thus H₅(P ! ll) = H₁(k,P,ll) from CQC_LANG:sch 6(A1); :: thesis: verum