set k = len l;
set QCP = { Q where Q is QC-pred_symbol of A : the_arity_of Q = len l } ;
P in { Q where Q is QC-pred_symbol of A : the_arity_of Q = 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;
A2: QC-WFF A is non empty A -closed set by Def11;
for D being non empty A -closed set holds <*P*> ^ l in D by Def10;
hence <*P*> ^ l is Element of QC-WFF A by A2; :: thesis: verum