let Al be QC-alphabet ; :: thesis: 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
let k be Nat; :: thesis: 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
let P be QC-pred_symbol of k,Al; :: thesis: 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
let k, l be Nat; :: thesis: ( P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al implies k = l )
assume A1: ( P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al ) ; :: thesis: k = l
then P in l -ary_QC-pred_symbols Al ;
then P in { P2 where P2 is Element of QC-pred_symbols Al : the_arity_of P2 = l } by QC_LANG1:def 9;
then A2: ex P2 being Element of QC-pred_symbols Al st
( P2 = P & the_arity_of P2 = l ) ;
P in k -ary_QC-pred_symbols Al by A1;
then P in { P1 where P1 is Element of QC-pred_symbols Al : the_arity_of P1 = k } by QC_LANG1:def 9;
then ex P1 being Element of QC-pred_symbols Al st
( P1 = P & the_arity_of P1 = k ) ;
hence k = l by A2; :: thesis: verum