theorem :: QC_LANG3:54

for k being Nat
for A being QC-alphabet
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds Free (P ! l) = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } by Th37;