let f be one-to-one PartFunc of REAL , REAL ; :: thesis: ( ( f | ([#] REAL ) is increasing or f | ([#] REAL ) is decreasing ) & f is total implies (f " ) | (rng f) is continuous )
set L = [#] REAL ;
assume that
A1: ( f | ([#] REAL ) is increasing or f | ([#] REAL ) is decreasing ) and
A2: f is total ; :: thesis: (f " ) | (rng f) is continuous
A3: dom f = [#] REAL by A2, PARTFUN1:def 4;

now

per cases ( f | ([#] REAL ) is increasing or f | ([#] REAL ) is decreasing ) by A1;

suppose f | ([#] REAL ) is increasing ; :: thesis: (f " ) | (rng f) is continuous

then ((f | ([#] REAL )) " ) | (f .: ([#] REAL )) is increasing by Th17;
then ((f | ([#] REAL )) " ) | (f .: ([#] REAL )) is non-decreasing ;
then A4: ((f | ([#] REAL )) " ) | (f .: ([#] REAL )) is monotone ;

now

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

end;

then A6: f .: ([#] REAL ) c= dom ((f | ([#] REAL )) " ) by SUBSET_1:7;
((f | ([#] REAL )) " ) .: (f .: ([#] REAL )) = ((f | ([#] REAL )) " ) .: (rng (f | ([#] REAL ))) by RELAT_1:148
.= ((f | ([#] REAL )) " ) .: (dom ((f | ([#] REAL )) " )) by FUNCT_1:55
.= rng ((f | ([#] REAL )) " ) by RELAT_1:146
.= dom (f | ([#] REAL )) by FUNCT_1:55
.= (dom f) /\ ([#] REAL ) by RELAT_1:90
.= REAL by A3 ;
then ((f | ([#] REAL )) " ) | (f .: ([#] REAL )) is continuous by A4, A6, Th24;
then ((f | ([#] REAL )) " ) | (rng f) is continuous by A3, RELAT_1:146;
hence (f " ) | (rng f) is continuous by A3, RELAT_1:97; :: thesis: verum

end;

suppose f | ([#] REAL ) is decreasing ; :: thesis: (f " ) | (rng f) is continuous

then ((f | ([#] REAL )) " ) | (f .: ([#] REAL )) is decreasing by Th18;
then ((f | ([#] REAL )) " ) | (f .: ([#] REAL )) is non-increasing ;
then A7: ((f | ([#] REAL )) " ) | (f .: ([#] REAL )) is monotone ;

now

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

end;

then A9: f .: ([#] REAL ) c= dom ((f | ([#] REAL )) " ) by SUBSET_1:7;
((f | ([#] REAL )) " ) .: (f .: ([#] REAL )) = ((f | ([#] REAL )) " ) .: (rng (f | ([#] REAL ))) by RELAT_1:148
.= ((f | ([#] REAL )) " ) .: (dom ((f | ([#] REAL )) " )) by FUNCT_1:55
.= rng ((f | ([#] REAL )) " ) by RELAT_1:146
.= dom (f | ([#] REAL )) by FUNCT_1:55
.= (dom f) /\ ([#] REAL ) by RELAT_1:90
.= REAL by A3 ;
then ((f | ([#] REAL )) " ) | (f .: ([#] REAL )) is continuous by A7, A9, Th24;
then ((f | ([#] REAL )) " ) | (rng f) is continuous by A3, RELAT_1:146;
hence (f " ) | (rng f) is continuous by A3, RELAT_1:97; :: thesis: verum

end;

end;

end;

hence (f " ) | (rng f) is continuous ; :: thesis: verum