let f be one-to-one continuous Function of R^1 ,R^1 ; :: thesis: for g being PartFunc of REAL , REAL st [.0 ,1.] c= dom f & f = g & not g | [.0 ,1.] is increasing holds
g | [.0 ,1.] is decreasing
let g be PartFunc of REAL , REAL ; :: thesis: ( [.0 ,1.] c= dom f & f = g & not g | [.0 ,1.] is increasing implies g | [.0 ,1.] is decreasing )
assume Z: [.0 ,1.] c= dom f ; :: 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 g | REAL is continuous by Th8;
then g | [.0 ,1.] is continuous by FCONT_1:17;
then ( g | [.0 ,1.] is increasing or g | [.0 ,1.] is decreasing ) by A1, Z, FCONT_2:18;
hence ( g | [.0 ,1.] is increasing or g | [.0 ,1.] is decreasing ) ; :: thesis: verum