theorem :: SUBSTUT2:3

for Al being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,Al
for k, l being Nat st P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al holds
k = l by Lm1;