let f be real-valued Function; :: thesis: ( f is one-to-one & f is non-decreasing implies f is increasing )
assume A1: ( f is one-to-one & f is non-decreasing ) ; :: thesis: f is increasing
for e1, e2 being ExtReal st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 < f . e2
proof
let e1, e2 be ExtReal; :: thesis: ( e1 in dom f & e2 in dom f & e1 < e2 implies f . e1 < f . e2 )
assume A2: ( e1 in dom f & e2 in dom f & e1 < e2 ) ; :: thesis: f . e1 < f . e2
f . e1 <= f . e2 by A1, A2, VALUED_0:def 15;
hence f . e1 < f . e2 by XXREAL_0:1, A2, A1; :: thesis: verum
end;
hence f is increasing by VALUED_0:def 13; :: thesis: verum