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<sub>1</sub>[k] } ;
A1: { k where k is Element of NAT : S<sub>1</sub>[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: ( not a in { k where k is Element of NAT : S₁[k] } or a in len p )
assume a in { k where k is Element of NAT : S₁[k] } ; :: thesis: a in len p
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: not len q = 0

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

end;

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

now :: thesis: not k >= len p

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

end;

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

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: 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 )
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: verum