theorem Th8: :: SUBLEMMA:8

for Al being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds CQC_Sub (Sub_P (P,ll,Sub)) = P ! (CQC_Subst (ll,Sub))