set r = <%(- x),(1. L)%>;
defpred S1[ 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 : S1[k] } ;
A1: { k where k is Element of NAT : S1[k] } c= NAT from 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 : S1[k] } ;
A3: len p > 0 by Th14;
{ k where k is Element of NAT : S1[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 : S1[k] } or a in len p )
assume a in { k where k is Element of NAT : S1[k] } ; :: thesis: a in len p
then consider k being Element of NAT such that
A4: a = k and
A5: S1[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 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 ;
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 ; :: thesis: verum
end;
then reconsider F = { k where k is Element of NAT : S1[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