let p be Real; :: thesis: for f being one-to-one PartFunc of REAL ,REAL st ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) & left_open_halfline p c= dom f holds
((f | (left_open_halfline p)) " ) | (f .: (left_open_halfline p)) is continuous
let f be one-to-one PartFunc of REAL ,REAL ; :: thesis: ( ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) & left_open_halfline p c= dom f implies ((f | (left_open_halfline p)) " ) | (f .: (left_open_halfline p)) is continuous )
set L = left_open_halfline p;
assume that
A1: ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) and
A2: left_open_halfline p c= dom f ; :: thesis: ((f | (left_open_halfline p)) " ) | (f .: (left_open_halfline p)) is continuous

now

per cases ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) by A1;

suppose f | (left_open_halfline p) is increasing ; :: thesis: ((f | (left_open_halfline p)) " ) | (f .: (left_open_halfline p)) is continuous

then ((f | (left_open_halfline p)) " ) | (f .: (left_open_halfline p)) is increasing by Th17;
then ((f | (left_open_halfline p)) " ) | (f .: (left_open_halfline p)) is non-decreasing ;
then A3: ((f | (left_open_halfline p)) " ) | (f .: (left_open_halfline p)) is monotone ;

now

let r be Real; :: thesis: ( r in f .: (left_open_halfline p) implies r in dom ((f | (left_open_halfline p)) " ) )
assume r in f .: (left_open_halfline p) ; :: thesis: r in dom ((f | (left_open_halfline p)) " )
then consider s being Real such that
A4: ( s in dom f & s in left_open_halfline p & r = f . s ) by PARTFUN2:78;
( s in (dom f) /\ (left_open_halfline p) & r = f . s ) by A4, XBOOLE_0:def 4;
then ( s in dom (f | (left_open_halfline p)) & r = f . s ) by RELAT_1:90;
then ( s in dom (f | (left_open_halfline p)) & r = (f | (left_open_halfline p)) . s ) by FUNCT_1:70;
then r in rng (f | (left_open_halfline p)) by FUNCT_1:def 5;
hence r in dom ((f | (left_open_halfline p)) " ) by FUNCT_1:55; :: thesis: verum

end;

then A5: f .: (left_open_halfline p) c= dom ((f | (left_open_halfline p)) " ) by SUBSET_1:7;
((f | (left_open_halfline p)) " ) .: (f .: (left_open_halfline p)) = ((f | (left_open_halfline p)) " ) .: (rng (f | (left_open_halfline p))) by RELAT_1:148
.= ((f | (left_open_halfline p)) " ) .: (dom ((f | (left_open_halfline p)) " )) by FUNCT_1:55
.= rng ((f | (left_open_halfline p)) " ) by RELAT_1:146
.= dom (f | (left_open_halfline p)) by FUNCT_1:55
.= (dom f) /\ (left_open_halfline p) by RELAT_1:90
.= left_open_halfline p by A2, XBOOLE_1:28 ;
hence ((f | (left_open_halfline p)) " ) | (f .: (left_open_halfline p)) is continuous by A3, A5, Th19; :: thesis: verum

end;

suppose f | (left_open_halfline p) is decreasing ; :: thesis: ((f | (left_open_halfline p)) " ) | (f .: (left_open_halfline p)) is continuous

then ((f | (left_open_halfline p)) " ) | (f .: (left_open_halfline p)) is decreasing by Th18;
then ((f | (left_open_halfline p)) " ) | (f .: (left_open_halfline p)) is non-increasing ;
then A6: ((f | (left_open_halfline p)) " ) | (f .: (left_open_halfline p)) is monotone ;

now

let r be Real; :: thesis: ( r in f .: (left_open_halfline p) implies r in dom ((f | (left_open_halfline p)) " ) )
assume r in f .: (left_open_halfline p) ; :: thesis: r in dom ((f | (left_open_halfline p)) " )
then consider s being Real such that
A7: ( s in dom f & s in left_open_halfline p & r = f . s ) by PARTFUN2:78;
s in (dom f) /\ (left_open_halfline p) by A7, XBOOLE_0:def 4;
then s in dom (f | (left_open_halfline p)) by RELAT_1:90;
then ( s in dom (f | (left_open_halfline p)) & r = (f | (left_open_halfline p)) . s ) by A7, FUNCT_1:70;
then r in rng (f | (left_open_halfline p)) by FUNCT_1:def 5;
hence r in dom ((f | (left_open_halfline p)) " ) by FUNCT_1:55; :: thesis: verum

end;

then A8: f .: (left_open_halfline p) c= dom ((f | (left_open_halfline p)) " ) by SUBSET_1:7;
((f | (left_open_halfline p)) " ) .: (f .: (left_open_halfline p)) = ((f | (left_open_halfline p)) " ) .: (rng (f | (left_open_halfline p))) by RELAT_1:148
.= ((f | (left_open_halfline p)) " ) .: (dom ((f | (left_open_halfline p)) " )) by FUNCT_1:55
.= rng ((f | (left_open_halfline p)) " ) by RELAT_1:146
.= dom (f | (left_open_halfline p)) by FUNCT_1:55
.= (dom f) /\ (left_open_halfline p) by RELAT_1:90
.= left_open_halfline p by A2, XBOOLE_1:28 ;
hence ((f | (left_open_halfline p)) " ) | (f .: (left_open_halfline p)) is continuous by A6, A8, Th19; :: thesis: verum

end;

end;

end;

hence ((f | (left_open_halfline p)) " ) | (f .: (left_open_halfline p)) is continuous ; :: thesis: verum