set L = [#] REAL;
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 )
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 2;

now :: thesis: (f ") | (rng f) is continuous

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

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

A5: now :: thesis: for r being Element of REAL st r in f .: ([#] REAL) holds
r in dom ((f | ([#] REAL)) ")

let r be Element of 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 Element of REAL such that
A6: s in dom f and
s in [#] REAL and
A7: r = f . s by PARTFUN2:59;
s in (dom f) /\ ([#] REAL) by A6, XBOOLE_0:def 4;
then A8: s in dom (f | ([#] REAL)) by RELAT_1:61;
r = (f | ([#] REAL)) . s by A7;
then r in rng (f | ([#] REAL)) by A8, FUNCT_1:def 3;
hence r in dom ((f | ([#] REAL)) ") by FUNCT_1:33; :: thesis: verum

end;

A9: ((f | ([#] REAL)) ") .: (f .: ([#] REAL)) = ((f | ([#] REAL)) ") .: (rng (f | ([#] REAL))) by RELAT_1:115
.= ((f | ([#] REAL)) ") .: (dom ((f | ([#] REAL)) ")) by FUNCT_1:33
.= rng ((f | ([#] REAL)) ") by RELAT_1:113
.= dom (f | ([#] REAL)) by FUNCT_1:33
.= (dom f) /\ ([#] REAL) by RELAT_1:61
.= REAL by A3 ;
((f | ([#] REAL)) ") | (f .: ([#] REAL)) is increasing by A4, Th9;
then ((f | ([#] REAL)) ") | (f .: ([#] REAL)) is continuous by A5, A9, Th16, SUBSET_1:2;
then ((f | ([#] REAL)) ") | (rng f) is continuous by A3, RELAT_1:113;
hence (f ") | (rng f) is continuous ; :: thesis: verum

end;

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

A11: now :: thesis: for r being Element of REAL st r in f .: ([#] REAL) holds
r in dom ((f | ([#] REAL)) ")

let r be Element of 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 Element of REAL such that
A12: s in dom f and
s in [#] REAL and
A13: r = f . s by PARTFUN2:59;
s in (dom f) /\ ([#] REAL) by A12, XBOOLE_0:def 4;
then A14: s in dom (f | ([#] REAL)) by RELAT_1:61;
r = (f | ([#] REAL)) . s by A13;
then r in rng (f | ([#] REAL)) by A14, FUNCT_1:def 3;
hence r in dom ((f | ([#] REAL)) ") by FUNCT_1:33; :: thesis: verum

end;

A15: ((f | ([#] REAL)) ") .: (f .: ([#] REAL)) = ((f | ([#] REAL)) ") .: (rng (f | ([#] REAL))) by RELAT_1:115
.= ((f | ([#] REAL)) ") .: (dom ((f | ([#] REAL)) ")) by FUNCT_1:33
.= rng ((f | ([#] REAL)) ") by RELAT_1:113
.= dom (f | ([#] REAL)) by FUNCT_1:33
.= (dom f) /\ ([#] REAL) by RELAT_1:61
.= REAL by A3 ;
((f | ([#] REAL)) ") | (f .: ([#] REAL)) is decreasing by A10, Th10;
then ((f | ([#] REAL)) ") | (f .: ([#] REAL)) is continuous by A11, A15, Th16, SUBSET_1:2;
then ((f | ([#] REAL)) ") | (rng f) is continuous by A3, RELAT_1:113;
hence (f ") | (rng f) is continuous ; :: thesis: verum

end;

end;

end;

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