theorem :: CQC_SIM1:15

for A being QC-alphabet
for k being Nat
for ll being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds QuantNbr (P ! ll) = 0