set k = len l;
set QCP = { Q where Q is QC-pred_symbol : the_arity_of Q = len l } ;
( { Q where Q is QC-pred_symbol : the_arity_of Q = len l } = (len l) -ary_QC-pred_symbols & 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 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