I c= I
;

then reconsider I9 = I as non empty Subset of I ;

defpred S_{1}[ Element of I, Element of NAT ] means for p being Polynomial of L st $1 = p holds

$2 = len p;

set u = { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds

len x9 <= len y9 } ;

A2: for x being Element of I holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A1);

min (f .: I9) in f .: I by XXREAL_2:def 7;

then consider x being object such that

A3: x in dom f and

x in I and

A4: min (f .: I9) = f . x by FUNCT_1:def 6;

reconsider x = x as Element of I by A3;

len x9 <= len y9 } ;

{ x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds

len x9 <= len y9 } c= I

len x9 <= len y9 } is non empty Subset of I by A7; :: thesis: verum

then reconsider I9 = I as non empty Subset of I ;

defpred S

$2 = len p;

set u = { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds

len x9 <= len y9 } ;

A1: now :: thesis: for x being Element of I ex y being Element of NAT st S_{1}[x,y]

consider f being Function of I,NAT such that let x be Element of I; :: thesis: ex y being Element of NAT st S_{1}[x,y]

reconsider x9 = x as Polynomial of L by POLYNOM3:def 10;

for p being Polynomial of L st x = p holds

len x9 = len p ;

hence ex y being Element of NAT st S_{1}[x,y]
; :: thesis: verum

end;reconsider x9 = x as Polynomial of L by POLYNOM3:def 10;

for p being Polynomial of L st x = p holds

len x9 = len p ;

hence ex y being Element of NAT st S

A2: for x being Element of I holds S

min (f .: I9) in f .: I by XXREAL_2:def 7;

then consider x being object such that

A3: x in dom f and

x in I and

A4: min (f .: I9) = f . x by FUNCT_1:def 6;

reconsider x = x as Element of I by A3;

now :: thesis: for x9, y9 being Polynomial of L st x9 = x & y9 in I holds

len x9 <= len y9

then A7:
x in { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds len x9 <= len y9

let x9, y9 be Polynomial of L; :: thesis: ( x9 = x & y9 in I implies len x9 <= len y9 )

assume that

A5: x9 = x and

A6: y9 in I ; :: thesis: len x9 <= len y9

dom f = I by FUNCT_2:def 1;

then f . y9 in f .: I by A6, FUNCT_1:def 6;

then f . x <= f . y9 by A4, XXREAL_2:def 7;

then len x9 <= f . y9 by A2, A5;

hence len x9 <= len y9 by A2, A6; :: thesis: verum

end;assume that

A5: x9 = x and

A6: y9 in I ; :: thesis: len x9 <= len y9

dom f = I by FUNCT_2:def 1;

then f . y9 in f .: I by A6, FUNCT_1:def 6;

then f . x <= f . y9 by A4, XXREAL_2:def 7;

then len x9 <= f . y9 by A2, A5;

hence len x9 <= len y9 by A2, A6; :: thesis: verum

len x9 <= len y9 } ;

{ x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds

len x9 <= len y9 } c= I

proof

hence
{ x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds

len x9 <= len y9 } or x in I )

assume x in { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds

len x9 <= len y9 } ; :: thesis: x in I

then ex x99 being Element of I st

( x99 = x & ( for x9, y9 being Polynomial of L st x9 = x99 & y9 in I holds

len x9 <= len y9 ) ) ;

hence x in I ; :: thesis: verum

end;len x9 <= len y9 } or x in I )

assume x in { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds

len x9 <= len y9 } ; :: thesis: x in I

then ex x99 being Element of I st

( x99 = x & ( for x9, y9 being Polynomial of L st x9 = x99 & y9 in I holds

len x9 <= len y9 ) ) ;

hence x in I ; :: thesis: verum

len x9 <= len y9 } is non empty Subset of I by A7; :: thesis: verum