set N = { i where i is Element of NAT : f . i = b } ;

consider x being object such that

A3: x in NAT and

A4: f . x = b by A1, A2, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A3;

A5: x in { i where i is Element of NAT : f . i = b } by A4;

take I = min N; :: thesis: ( f . I = b & ( for i being Element of NAT st f . i = b holds

I <= i ) )

I in N by XXREAL_2:def 7;

then ex II being Element of NAT st

( II = I & f . II = b ) ;

hence f . I = b ; :: thesis: for i being Element of NAT st f . i = b holds

I <= i

let i be Element of NAT ; :: thesis: ( f . i = b implies I <= i )

assume f . i = b ; :: thesis: I <= i

then i in N ;

hence I <= i by XXREAL_2:def 7; :: thesis: verum

consider x being object such that

A3: x in NAT and

A4: f . x = b by A1, A2, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A3;

A5: x in { i where i is Element of NAT : f . i = b } by A4;

now :: thesis: for x being object st x in { i where i is Element of NAT : f . i = b } holds

x in NAT

then reconsider N = { i where i is Element of NAT : f . i = b } as non empty Subset of NAT by A5, TARSKI:def 3;x in NAT

let x be object ; :: thesis: ( x in { i where i is Element of NAT : f . i = b } implies x in NAT )

assume x in { i where i is Element of NAT : f . i = b } ; :: thesis: x in NAT

then ex i being Element of NAT st

( x = i & f . i = b ) ;

hence x in NAT ; :: thesis: verum

end;assume x in { i where i is Element of NAT : f . i = b } ; :: thesis: x in NAT

then ex i being Element of NAT st

( x = i & f . i = b ) ;

hence x in NAT ; :: thesis: verum

take I = min N; :: thesis: ( f . I = b & ( for i being Element of NAT st f . i = b holds

I <= i ) )

I in N by XXREAL_2:def 7;

then ex II being Element of NAT st

( II = I & f . II = b ) ;

hence f . I = b ; :: thesis: for i being Element of NAT st f . i = b holds

I <= i

let i be Element of NAT ; :: thesis: ( f . i = b implies I <= i )

assume f . i = b ; :: thesis: I <= i

then i in N ;

hence I <= i by XXREAL_2:def 7; :: thesis: verum