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 )
then ( dom f = REAL & g is continuous ) by Th8, FUNCT_2:def 1, TOPMETR:24;
hence ( g | [.0 ,1.] is increasing or g | [.0 ,1.] is decreasing ) by A1, FCONT_2:18; :: thesis: verum