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

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