let IT1, IT2 be Element of NAT ; :: thesis: ( f . IT1 = b & m < IT1 & ( for i being Element of NAT st m < i & f . i = b holds
IT1 <= i ) & f . IT2 = b & m < IT2 & ( for i being Element of NAT st m < i & f . i = b holds
IT2 <= i ) implies IT1 = IT2 )
assume that
A7: f . IT1 = b and
A8: m < IT1 and
A9: for i being Element of NAT st m < i & f . i = b holds
IT1 <= i and
A10: f . IT2 = b and
A11: m < IT2 and
A12: for i being Element of NAT st m < i & f . i = b holds
IT2 <= i ; :: thesis: IT1 = IT2
assume A13: IT1 <> IT2 ; :: thesis: contradiction

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

suppose IT1 < IT2 ; :: thesis: contradiction

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

end;

suppose IT1 > IT2 ; :: thesis: contradiction

hence contradiction by A9, A10, A11; :: thesis: verum

end;

end;