theorem Th15: :: SUBSTUT2:15

for Al being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub])