consider k being Element of NAT , P being QC-pred_symbol of k, ll being QC-variable_list of k such that
A2: F = P ! ll by A1, Def17;
reconsider ll = ll as FinSequence of QC-variables ;
take ll ; :: thesis: ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being QC-variable_list of k st
( ll = ll & F = P ! ll )
thus ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being QC-variable_list of k st
( ll = ll & F = P ! ll ) by A2; :: thesis: verum