set r = <%(- x),(1. L)%>;

defpred S_{1}[ 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_{1}[k] } ;

A1: { k where k is Element of NAT : S_{1}[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_{1}[k] }
;

A3: len p > 0 by Th14;

{ k where k is Element of NAT : S_{1}[k] } c= len p
_{1}[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

defpred S

set F = { k where k is Element of NAT : S

A1: { k where k is Element of NAT : S

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

A3: len p > 0 by Th14;

{ k where k is Element of NAT : S

proof

then reconsider F = { k where k is Element of NAT : S
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { k where k is Element of NAT : S_{1}[k] } or a in len p )

assume a in { k where k is Element of NAT : S_{1}[k] }
; :: thesis: a in len p

then consider k being Element of NAT such that

A4: a = k and

A5: S_{1}[k]
;

consider q being Polynomial of L such that

A6: p = (<%(- x),(1. L)%> `^ k) *' q by A5;

hence a in len p by A4, AXIOMS:4; :: thesis: verum

end;assume a in { k where k is Element of NAT : S

then consider k being Element of NAT such that

A4: a = k and

A5: S

consider q being Polynomial of L such that

A6: p = (<%(- x),(1. L)%> `^ k) *' q by A5;

A7: now :: thesis: not len q = 0

then reconsider q = q as non-zero Polynomial of L by Th14;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 q = 0_. L by POLYNOM4:5;

then p = 0_. L by A6, POLYNOM4:2;

hence contradiction by A3, POLYNOM4:3; :: thesis: verum

now :: thesis: not k >= len p

then
k in { i where i is Nat : i < 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 + (len q) > (len p) + 0 by A7, XREAL_1:8;

hence contradiction by A6, Th37; :: thesis: verum

hence a in len p by A4, AXIOMS:4; :: thesis: verum

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