set k = len l;
set QCP = { Q where Q is QC-pred_symbol : the_arity_of Q = len l } ;
P in { Q where Q is QC-pred_symbol : the_arity_of Q = len l } by A1;
then reconsider P = P as QC-pred_symbol of (len l) ;
reconsider l = l as QC-variable_list of len l by FINSEQ_1:def 18;
reconsider X = <*P*> ^ l as FinSequence of [:NAT ,NAT :] by Lm2;
X is QC-formula by Def9, Th21;
hence <*P*> ^ l is Element of QC-WFF ; :: thesis: verum