consider k being Element of NAT , P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A, e being Element of vSUB A such that
A1: S = Sub_P (P,ll,e) by B1, Def25;
reconsider ll = ll as FinSequence of QC-variables A ;
take ll ; :: thesis: ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( ll = ll & S = Sub_P (P,ll,e) )
thus ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( ll = ll & S = Sub_P (P,ll,e) ) by A1; :: thesis: verum