let A be QC-alphabet ; :: thesis: for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds p ! ll = <*p*> ^ ll
let k be Nat; :: thesis: for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds p ! ll = <*p*> ^ ll
let p be QC-pred_symbol of k,A; :: thesis: for ll being QC-variable_list of k,A holds p ! ll = <*p*> ^ ll
let ll be QC-variable_list of k,A; :: thesis: p ! ll = <*p*> ^ ll
set QCP = { Q where Q is QC-pred_symbol of A : the_arity_of Q = k } ;
p in { Q where Q is QC-pred_symbol of A : the_arity_of Q = k } ;
then A1: ex Q being QC-pred_symbol of A st
( p = Q & the_arity_of Q = k ) ;
len ll = k by CARD_1:def 7;
hence p ! ll = <*p*> ^ ll by A1, Def12; :: thesis: verum