set k = len l;
set QCP = { QP where QP is QC-pred_symbol : the_arity_of QP = len l } ;
P in { QP where QP is QC-pred_symbol : the_arity_of QP = 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 CARD_1:def 7;
P ! l = <*P*> ^ l by QC_LANG1:6;
hence [(P ! l),e] is Element of QC-Sub-WFF by Def16; :: thesis: verum