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