let f be real-valued Function; :: thesis: ( f is NAT -defined & f is increasing implies f is one-to-one )
assume that
A0: f is NAT -defined and
A1: f is increasing ; :: thesis: f is one-to-one
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A2: ( x in dom f & y in dom f ) and
A3: f . x = f . y ; :: thesis: x = y
dom f c= NAT by A0, RELAT_1:def 18;
then reconsider x = x, y = y as Element of NAT by A2;
( x <= y & x >= y ) by A1, A2, A3, VALUED_0:def 13;
hence x = y by XXREAL_0:1; :: thesis: verum