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
A6: f . IT1 = b and
A7: for i being Element of NAT st f . i = b holds
IT1 <= i and
A8: f . IT2 = b and
A9: for i being Element of NAT st f . i = b holds
IT2 <= i ; :: thesis: IT1 = IT2
assume A10: IT1 <> IT2 ; :: thesis: contradiction

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

suppose IT1 < IT2 ; :: thesis: contradiction

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

end;

suppose IT1 > IT2 ; :: thesis: contradiction

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

end;

end;