let k be Element of NAT ; :: thesis: for p being QC-pred_symbol of k
for ll being QC-variable_list of holds p ! ll = <*p*> ^ ll
let p be QC-pred_symbol of k; :: thesis: for ll being QC-variable_list of holds p ! ll = <*p*> ^ ll
let ll be QC-variable_list of ; :: thesis: p ! ll = <*p*> ^ ll
set QCP = { Q where Q is QC-pred_symbol : the_arity_of Q = k } ;
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 ) ;
then ( len ll = k & the_arity_of p = k ) by FINSEQ_1:def 18;
hence p ! ll = <*p*> ^ ll by Def11; :: thesis: verum