let f be one-to-one continuous Function of R^1 ,R^1 ; :: thesis: for g being PartFunc of REAL ,REAL holds
( not f = g or g | [.0 ,1.] is increasing or g | [.0 ,1.] is decreasing )
let g be PartFunc of REAL ,REAL ; :: thesis: ( not f = g or g | [.0 ,1.] is increasing or g | [.0 ,1.] is decreasing )
assume A1: f = g ; :: thesis: ( g | [.0 ,1.] is increasing or g | [.0 ,1.] is decreasing )
Z: dom f = REAL by FUNCT_2:def 1, TOPMETR:24;
g is continuous by A1, Th8;
then g | [.0 ,1.] is continuous ;
hence ( g | [.0 ,1.] is increasing or g | [.0 ,1.] is decreasing ) by A1, Z, FCONT_2:18; :: thesis: verum