set N = { i where i is Element of NAT : ( m < i & f . i = b ) } ;
consider j being Element of NAT such that
A2: m < j and
A3: f . j = b by A1;
A4: j in { i where i is Element of NAT : ( m < i & f . i = b ) } by A2, A3;

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

let x be object ; :: thesis: ( x in { i where i is Element of NAT : ( m < i & f . i = b ) } implies x in NAT )
assume x in { i where i is Element of NAT : ( m < i & f . i = b ) } ; :: thesis: x in NAT
then ex i being Element of NAT st
( x = i & m < i & f . i = b ) ;
hence x in NAT ; :: thesis: verum

end;

then reconsider N = { i where i is Element of NAT : ( m < i & f . i = b ) } as non empty Subset of NAT by A4, TARSKI:def 3;
take I = min N; :: thesis: ( f . I = b & m < I & ( for i being Element of NAT st m < i & f . i = b holds
I <= i ) )
I in N by XXREAL_2:def 7;
then ex II being Element of NAT st
( II = I & m < II & f . II = b ) ;
hence ( f . I = b & m < I ) ; :: thesis: for i being Element of NAT st m < i & f . i = b holds
I <= i
let i be Element of NAT ; :: thesis: ( m < i & f . i = b implies I <= i )
assume that
A5: m < i and
A6: f . i = b ; :: thesis: I <= i
i in N by A5, A6;
hence I <= i by XXREAL_2:def 7; :: thesis: verum