theorem :: VALUAT_1:6

for Al being QC-alphabet
for k being Nat
for A being non empty set
for ll being CQC-variable_list of k,Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) by Lm1;