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

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