let Al be QC-alphabet ; :: thesis: for k being Nat
for P being QC-pred_symbol of k,Al
for Al2 being Al -expanding QC-alphabet holds P is QC-pred_symbol of k,Al2
let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al
for Al2 being Al -expanding QC-alphabet holds P is QC-pred_symbol of k,Al2
let P be QC-pred_symbol of k,Al; :: thesis: for Al2 being Al -expanding QC-alphabet holds P is QC-pred_symbol of k,Al2
let Al2 be Al -expanding QC-alphabet ; :: thesis: P is QC-pred_symbol of k,Al2
the_arity_of P = k by QC_LANG1:11;
then A1: P `1 = 7 + k by QC_LANG1:def 8;
reconsider P = P as QC-pred_symbol of Al2 by Th3, TARSKI:def 3;
the_arity_of P = k by QC_LANG1:def 8, A1;
hence P is QC-pred_symbol of k,Al2 by QC_LANG3:1; :: thesis: verum