theorem :: SUBSTUT2:14

for Al being QC-alphabet
for k being Nat
for x, y being bound_QC-variable of Al
for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al holds
( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) )