let p be Real; :: thesis: for f being one-to-one PartFunc of REAL,REAL st ( f | is increasing or f | is decreasing ) & right_closed_halfline p c= dom f holds
(() ") | () is continuous

let f be one-to-one PartFunc of REAL,REAL; :: thesis: ( ( f | is increasing or f | is decreasing ) & right_closed_halfline p c= dom f implies (() ") | () is continuous )
set L = right_closed_halfline p;
assume that
A1: ( f | is increasing or f | is decreasing ) and
A2: right_closed_halfline p c= dom f ; :: thesis: (() ") | () is continuous
now :: thesis: (() ") | () is continuous
per cases by A1;
suppose A3: f | is increasing ; :: thesis: (() ") | () is continuous
A4: now :: thesis: for r being Element of REAL st r in f .: holds
r in dom (() ")
let r be Element of REAL ; :: thesis: ( r in f .: implies r in dom (() ") )
assume r in f .: ; :: thesis: r in dom (() ")
then consider s being Element of REAL such that
A5: ( s in dom f & s in right_closed_halfline p ) and
A6: r = f . s by PARTFUN2:59;
s in (dom f) /\ by ;
then A7: s in dom () by RELAT_1:61;
then r = () . s by ;
then r in rng () by ;
hence r in dom (() ") by FUNCT_1:33; :: thesis: verum
end;
A8: (() ") .: () = (() ") .: (rng ()) by RELAT_1:115
.= (() ") .: (dom (() ")) by FUNCT_1:33
.= rng (() ") by RELAT_1:113
.= dom () by FUNCT_1:33
.= (dom f) /\ by RELAT_1:61
.= right_closed_halfline p by ;
((f | ) ") | () is increasing by ;
hence ((f | ) ") | () is continuous by ; :: thesis: verum
end;
suppose A9: f | is decreasing ; :: thesis: (() ") | () is continuous
A10: now :: thesis: for r being Element of REAL st r in f .: holds
r in dom (() ")
let r be Element of REAL ; :: thesis: ( r in f .: implies r in dom (() ") )
assume r in f .: ; :: thesis: r in dom (() ")
then consider s being Element of REAL such that
A11: ( s in dom f & s in right_closed_halfline p ) and
A12: r = f . s by PARTFUN2:59;
s in (dom f) /\ by ;
then A13: s in dom () by RELAT_1:61;
then r = () . s by ;
then r in rng () by ;
hence r in dom (() ") by FUNCT_1:33; :: thesis: verum
end;
A14: (() ") .: () = (() ") .: (rng ()) by RELAT_1:115
.= (() ") .: (dom (() ")) by FUNCT_1:33
.= rng (() ") by RELAT_1:113
.= dom () by FUNCT_1:33
.= (dom f) /\ by RELAT_1:61
.= right_closed_halfline p by ;
((f | ) ") | () is decreasing by ;
hence ((f | ) ") | () is continuous by ; :: thesis: verum
end;
end;
end;
hence ((f | ) ") | () is continuous ; :: thesis: verum