theorem Th2: :: SUBSTUT2:2

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 ex S being Element of CQC-Sub-WFF Al st
( S `1 = P ! ll & S `2 = Sub )