set k = len l;
set QCP = { QP where QP is QC-pred_symbol of A : the_arity_of QP = len l } ;
P in { QP where QP is QC-pred_symbol of A : the_arity_of QP = len l } by A1;
then reconsider P = P as QC-pred_symbol of (len l),A ;
reconsider l = l as QC-variable_list of len l,A by CARD_1:def 7;
P ! l = <*P*> ^ l by QC_LANG1:8;
hence [(P ! l),e] is Element of QC-Sub-WFF A by Def16; :: thesis: verum