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

((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous

let f be one-to-one PartFunc of REAL,REAL; :: thesis: ( ( f | (left_closed_halfline p) is increasing or f | (left_closed_halfline p) is decreasing ) & left_closed_halfline p c= dom f implies ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous )

set L = left_closed_halfline p;

assume that

A1: ( f | (left_closed_halfline p) is increasing or f | (left_closed_halfline p) is decreasing ) and

A2: left_closed_halfline p c= dom f ; :: thesis: ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous

((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous

let f be one-to-one PartFunc of REAL,REAL; :: thesis: ( ( f | (left_closed_halfline p) is increasing or f | (left_closed_halfline p) is decreasing ) & left_closed_halfline p c= dom f implies ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous )

set L = left_closed_halfline p;

assume that

A1: ( f | (left_closed_halfline p) is increasing or f | (left_closed_halfline p) is decreasing ) and

A2: left_closed_halfline p c= dom f ; :: thesis: ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous

now :: thesis: ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous end;

hence
((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous
; :: thesis: verumper cases
( f | (left_closed_halfline p) is increasing or f | (left_closed_halfline p) is decreasing )
by A1;

end;

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

.= ((f | (left_closed_halfline p)) ") .: (dom ((f | (left_closed_halfline p)) ")) by FUNCT_1:33

.= rng ((f | (left_closed_halfline p)) ") by RELAT_1:113

.= dom (f | (left_closed_halfline p)) by FUNCT_1:33

.= (dom f) /\ (left_closed_halfline p) by RELAT_1:61

.= left_closed_halfline p by A2, XBOOLE_1:28 ;

((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is increasing by A3, Th9;

hence ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous by A4, A8, Th13, SUBSET_1:2; :: thesis: verum

end;

A4: now :: thesis: for r being Element of REAL st r in f .: (left_closed_halfline p) holds

r in dom ((f | (left_closed_halfline p)) ")

A8: ((f | (left_closed_halfline p)) ") .: (f .: (left_closed_halfline p)) =
((f | (left_closed_halfline p)) ") .: (rng (f | (left_closed_halfline p)))
by RELAT_1:115
r in dom ((f | (left_closed_halfline p)) ")

let r be Element of REAL ; :: thesis: ( r in f .: (left_closed_halfline p) implies r in dom ((f | (left_closed_halfline p)) ") )

assume r in f .: (left_closed_halfline p) ; :: thesis: r in dom ((f | (left_closed_halfline p)) ")

then consider s being Element of REAL such that

A5: ( s in dom f & s in left_closed_halfline p ) and

A6: r = f . s by PARTFUN2:59;

s in (dom f) /\ (left_closed_halfline p) by A5, XBOOLE_0:def 4;

then A7: s in dom (f | (left_closed_halfline p)) by RELAT_1:61;

then r = (f | (left_closed_halfline p)) . s by A6, FUNCT_1:47;

then r in rng (f | (left_closed_halfline p)) by A7, FUNCT_1:def 3;

hence r in dom ((f | (left_closed_halfline p)) ") by FUNCT_1:33; :: thesis: verum

end;assume r in f .: (left_closed_halfline p) ; :: thesis: r in dom ((f | (left_closed_halfline p)) ")

then consider s being Element of REAL such that

A5: ( s in dom f & s in left_closed_halfline p ) and

A6: r = f . s by PARTFUN2:59;

s in (dom f) /\ (left_closed_halfline p) by A5, XBOOLE_0:def 4;

then A7: s in dom (f | (left_closed_halfline p)) by RELAT_1:61;

then r = (f | (left_closed_halfline p)) . s by A6, FUNCT_1:47;

then r in rng (f | (left_closed_halfline p)) by A7, FUNCT_1:def 3;

hence r in dom ((f | (left_closed_halfline p)) ") by FUNCT_1:33; :: thesis: verum

.= ((f | (left_closed_halfline p)) ") .: (dom ((f | (left_closed_halfline p)) ")) by FUNCT_1:33

.= rng ((f | (left_closed_halfline p)) ") by RELAT_1:113

.= dom (f | (left_closed_halfline p)) by FUNCT_1:33

.= (dom f) /\ (left_closed_halfline p) by RELAT_1:61

.= left_closed_halfline p by A2, XBOOLE_1:28 ;

((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is increasing by A3, Th9;

hence ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous by A4, A8, Th13, SUBSET_1:2; :: thesis: verum

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

.= ((f | (left_closed_halfline p)) ") .: (dom ((f | (left_closed_halfline p)) ")) by FUNCT_1:33

.= rng ((f | (left_closed_halfline p)) ") by RELAT_1:113

.= dom (f | (left_closed_halfline p)) by FUNCT_1:33

.= (dom f) /\ (left_closed_halfline p) by RELAT_1:61

.= left_closed_halfline p by A2, XBOOLE_1:28 ;

((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is decreasing by A9, Th10;

hence ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous by A10, A14, Th13, SUBSET_1:2; :: thesis: verum

end;

A10: now :: thesis: for r being Element of REAL st r in f .: (left_closed_halfline p) holds

r in dom ((f | (left_closed_halfline p)) ")

A14: ((f | (left_closed_halfline p)) ") .: (f .: (left_closed_halfline p)) =
((f | (left_closed_halfline p)) ") .: (rng (f | (left_closed_halfline p)))
by RELAT_1:115
r in dom ((f | (left_closed_halfline p)) ")

let r be Element of REAL ; :: thesis: ( r in f .: (left_closed_halfline p) implies r in dom ((f | (left_closed_halfline p)) ") )

assume r in f .: (left_closed_halfline p) ; :: thesis: r in dom ((f | (left_closed_halfline p)) ")

then consider s being Element of REAL such that

A11: ( s in dom f & s in left_closed_halfline p ) and

A12: r = f . s by PARTFUN2:59;

s in (dom f) /\ (left_closed_halfline p) by A11, XBOOLE_0:def 4;

then A13: s in dom (f | (left_closed_halfline p)) by RELAT_1:61;

then r = (f | (left_closed_halfline p)) . s by A12, FUNCT_1:47;

then r in rng (f | (left_closed_halfline p)) by A13, FUNCT_1:def 3;

hence r in dom ((f | (left_closed_halfline p)) ") by FUNCT_1:33; :: thesis: verum

end;assume r in f .: (left_closed_halfline p) ; :: thesis: r in dom ((f | (left_closed_halfline p)) ")

then consider s being Element of REAL such that

A11: ( s in dom f & s in left_closed_halfline p ) and

A12: r = f . s by PARTFUN2:59;

s in (dom f) /\ (left_closed_halfline p) by A11, XBOOLE_0:def 4;

then A13: s in dom (f | (left_closed_halfline p)) by RELAT_1:61;

then r = (f | (left_closed_halfline p)) . s by A12, FUNCT_1:47;

then r in rng (f | (left_closed_halfline p)) by A13, FUNCT_1:def 3;

hence r in dom ((f | (left_closed_halfline p)) ") by FUNCT_1:33; :: thesis: verum

.= ((f | (left_closed_halfline p)) ") .: (dom ((f | (left_closed_halfline p)) ")) by FUNCT_1:33

.= rng ((f | (left_closed_halfline p)) ") by RELAT_1:113

.= dom (f | (left_closed_halfline p)) by FUNCT_1:33

.= (dom f) /\ (left_closed_halfline p) by RELAT_1:61

.= left_closed_halfline p by A2, XBOOLE_1:28 ;

((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is decreasing by A9, Th10;

hence ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous by A10, A14, Th13, SUBSET_1:2; :: thesis: verum