let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A holds QuantNbr ('not' p) = QuantNbr p

let p be Element of CQC-WFF A; :: thesis: QuantNbr ('not' p) = QuantNbr p

deffunc H_{5}( Element of CQC-WFF A) -> Element of NAT = QuantNbr $1;

A1: for p being Element of CQC-WFF A

for d being Element of NAT holds

( d = H_{5}(p) iff ex F being Function of (CQC-WFF A),NAT st

( d = F . p & F . (VERUM A) = 0 & ( for r, s being Element of CQC-WFF A

for x being Element of bound_QC-variables 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) = H_{1}(k,P,l) & F . ('not' r) = H_{2}(F . r) & F . (r '&' s) = H_{3}(F . r,F . s) & F . (All (x,r)) = H_{4}(x,F . r) ) ) ) )
by Def6;

thus H_{5}( 'not' p) = H_{2}(H_{5}(p))
from CQC_LANG:sch 7(A1); :: thesis: verum

let p be Element of CQC-WFF A; :: thesis: QuantNbr ('not' p) = QuantNbr p

deffunc H

A1: for p being Element of CQC-WFF A

for d being Element of NAT holds

( d = H

( d = F . p & F . (VERUM A) = 0 & ( for r, s being Element of CQC-WFF A

for x being Element of bound_QC-variables 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) = H

thus H