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 proj1 f or not y in proj1 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
reconsider nx = x, ny = y as Element of NAT by A2;
( nx <= ny & nx >= ny ) by A1, A2, A3, VALUED_0:def 13;
hence x = y by XXREAL_0:1; :: thesis: verum