let f be real-valued FinSequence; :: thesis: ( f is increasing implies f is one-to-one )
assume A1: f is increasing ; :: thesis: f is one-to-one
let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in K1(f) or not y in K1(f) or not f . x = f . y or x = y )
assume A2: ( x in dom f & y in dom f & f . x = f . y ) ; :: thesis: x = y
then reconsider nx = x, ny = y as Element of NAT ;
A3: nx <= ny by A1, A2, VALUED_0:def 13;
nx >= ny by A1, A2, VALUED_0:def 13;
hence x = y by A3, XXREAL_0:1; :: thesis: verum