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 ;
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
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:
then ex i being Element of NAT st
( x = i & f . i = b ) ;
hence x in NAT ; :: thesis: verum
end;
then reconsider N = { i where i is Element of NAT : f . i = b } as non empty Subset of NAT by ;
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