set r = <%(- x),(1. L)%>;
defpred S₁[ Element of NAT ] means ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ $1) *' q;
set F = { k where k is Element of NAT : S₁[k] } ;
A1: { k where k is Element of NAT : S₁[k] } c= NAT from FRAENKEL:sch 10();
p = (1_. L) *' p by POLYNOM3:35
.= (<%(- x),(1. L)%> `^ 0) *' p by POLYNOM5:15 ;
then A2: 0 in { k where k is Element of NAT : S₁[k] } ;
A3: len p > 0 by Th14;
{ k where k is Element of NAT : S₁[k] } c= len p

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in { k where k is Element of NAT : S₁[k] } ; :: thesis:
then consider k being Element of NAT such that
A4: a = k and
A5: S₁[k] ;
consider q being Polynomial of L such that
A6: p = (<%(- x),(1. L)%> `^ k) *' q by A5;

A7: now :: thesis:

assume len q = 0 ; :: thesis:
then q = 0_. L by POLYNOM4:5;
then p = 0_. L by A6, POLYNOM4:2;
hence contradiction by A3, POLYNOM4:3; :: thesis:

end;

then reconsider q = q as non-zero Polynomial of L by Th14;

now :: thesis:

assume k >= len p ; :: thesis:
then k + (len q) > (len p) + 0 by A7, XREAL_1:8;
hence contradiction by A6, Th37; :: thesis:

end;

then k in { i where i is Nat : i < len p } ;
hence a in len p by A4, AXIOMS:4; :: thesis:

end;

then reconsider F = { k where k is Element of NAT : S₁[k] } as non empty finite Subset of NAT by A2, A1;
reconsider FF = F as non empty finite natural-membered set ;
reconsider m = max FF as Element of NAT by ORDINAL1:def 12;
take m ; :: thesis:
thus ex F being non empty finite Subset of NAT st
( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & m = max F ) ; :: thesis: