theorem Th8: :: QC_LANG1:8

for A being QC-alphabet
for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds p ! ll = <*p*> ^ ll