let A be QC-alphabet ; :: thesis: for k being Nat
for P being QC-pred_symbol of k,A holds the_arity_of P = k
let k be Nat; :: thesis: for P being QC-pred_symbol of k,A holds the_arity_of P = k
let P be QC-pred_symbol of k,A; :: thesis: the_arity_of P = k
reconsider P = P as Element of k -ary_QC-pred_symbols A ;
P in { Q where Q is QC-pred_symbol of A : the_arity_of Q = k } ;
then ex Q being QC-pred_symbol of A st
( P = Q & the_arity_of Q = k ) ;
hence the_arity_of P = k ; :: thesis: verum