thus ( ex d being Element of NAT 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 bound_QC-variable of 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₁(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) ) ) ) & ( for d1, d2 being Element of NAT st ex F being Function of (CQC-WFF A),NAT st
( d1 = F . p & F . (VERUM A) = 0 & ( for r, s being Element of CQC-WFF A
for x being bound_QC-variable of 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₁(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) ) ) ) & ex F being Function of (CQC-WFF A),NAT st
( d2 = F . p & F . (VERUM A) = 0 & ( for r, s being Element of CQC-WFF A
for x being bound_QC-variable of 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₁(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) ) ) ) holds
d1 = d2 ) ) from CQC_LANG:sch 4(); :: thesis: verum