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 Th7, FUNCT_2:def 1, TOPMETR:17;
hence ( g | [.0,1.] is increasing or g | [.0,1.] is decreasing ) by A1, FCONT_2:17; :: thesis: verum