let k be Element of NAT ; :: thesis: for p being QC-pred_symbol of k
for ll being QC-variable_list of k holds p ! ll = <*p*> ^ ll
let p be QC-pred_symbol of k; :: thesis: for ll being QC-variable_list of k holds p ! ll = <*p*> ^ ll
let ll be QC-variable_list of k; :: 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 A1: ex Q being QC-pred_symbol st
( p = Q & the_arity_of Q = k ) ;
len ll = k by FINSEQ_1:def 18;
hence p ! ll = <*p*> ^ ll by A1, Def11; :: thesis: verum