let f be UnOp of [.0,1.]; :: thesis: ( f is non-decreasing iff for a, b being Element of [.0,1.] st a <= b holds
f . a <= f . b )
dom f = [.0,1.] by FUNCT_2:def 1;
hence ( f is non-decreasing implies for a, b being Element of [.0,1.] st a <= b holds
f . a <= f . b ) ; :: thesis: ( ( for a, b being Element of [.0,1.] st a <= b holds
f . a <= f . b ) implies f is non-decreasing )
assume B1: for a, b being Element of [.0,1.] st a <= b holds
f . a <= f . b ; :: thesis: f is non-decreasing
let e1, e2 be ExtReal; :: according to VALUED_0:def 15 :: thesis: ( not e1 in dom f or not e2 in dom f or not e1 <= e2 or f . e1 <= f . e2 )
assume B2: ( e1 in dom f & e2 in dom f & e1 <= e2 ) ; :: thesis: f . e1 <= f . e2
then reconsider ee1 = e1, ee2 = e2 as Element of [.0,1.] by FUNCT_2:def 1;
ee1 <= ee2 by B2;
hence f . e1 <= f . e2 by B1; :: thesis: verum