for A being QC-alphabet
for e being Element of vSUB A
for k being Nat
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e]