theorem Th17: :: CQC_LANG:17

for A being QC-alphabet
for x being bound_QC-variable of A
for k being Nat
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x)))