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;

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 end;

hence
(f ") | (rng f) is continuous
; :: thesis: verumper cases
( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing )
by A1;

end;

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

.= ((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;

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

r in dom ((f | ([#] REAL)) ")

A9: ((f | ([#] REAL)) ") .: (f .: ([#] REAL)) =
((f | ([#] REAL)) ") .: (rng (f | ([#] REAL)))
by RELAT_1:115
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;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

.= ((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

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

.= ((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;

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

r in dom ((f | ([#] REAL)) ")

A15: ((f | ([#] REAL)) ") .: (f .: ([#] REAL)) =
((f | ([#] REAL)) ") .: (rng (f | ([#] REAL)))
by RELAT_1:115
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;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

.= ((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