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;
then reconsider N = { i where i is Element of NAT : f . i = b } as non empty Subset of NAT by A5, TARSKI:def 3;
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