let IT1, IT2 be Element of NAT ; :: thesis: ( f . IT1 = b & ( for i being Element of NAT st f . i = b holds
IT1 <= i ) & f . IT2 = b & ( for i being Element of NAT st f . i = b holds
IT2 <= i ) implies IT1 = IT2 )
assume that
A4: f . IT1 = b and
A5: for i being Element of NAT st f . i = b holds
IT1 <= i and
A6: f . IT2 = b and
A7: for i being Element of NAT st f . i = b holds
IT2 <= i ; :: thesis: IT1 = IT2
assume A8: IT1 <> IT2 ; :: thesis: contradiction

per cases ( IT1 < IT2 or IT1 > IT2 ) by A8, XXREAL_0:1;

suppose IT1 < IT2 ; :: thesis: contradiction

hence contradiction by A4, A7; :: thesis: verum

end;

suppose IT1 > IT2 ; :: thesis: contradiction

hence contradiction by A5, A6; :: thesis: verum

end;

end;