consider k being Element of NAT , P being QC-pred_symbol of k, ll being QC-variable_list of , e being Element of vSUB such that
A2: S = Sub_P P,ll,e by A1, Def25;
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 ex e being Element of vSUB st
( ll = ll & S = Sub_P P,ll,e )
thus ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being QC-variable_list of ex e being Element of vSUB st
( ll = ll & S = Sub_P P,ll,e ) by A2; :: thesis: verum