set X = R^1 ;
let a, b be Real; :: thesis: for f being continuous Function of (Closed-Interval-TSpace (a,b)),R^1
for g being PartFunc of REAL,REAL st a <= b & f = g holds
g is continuous
set S = Closed-Interval-TSpace (a,b);
let f be continuous Function of (Closed-Interval-TSpace (a,b)),R^1; :: thesis: for g being PartFunc of REAL,REAL st a <= b & f = g holds
g is continuous
let g be PartFunc of REAL,REAL; :: thesis: ( a <= b & f = g implies g is continuous )
assume that
A1: a <= b and
A2: f = g ; :: thesis: g is continuous
set A = left_closed_halfline a;
set B = [.a,b.];
set C = right_closed_halfline b;
the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A1, TOPMETR:18;
then reconsider a1 = a, b1 = b as Point of (Closed-Interval-TSpace (a,b)) by A1, XXREAL_1:1;
set f1 = (R^1 | (R^1 (left_closed_halfline a))) --> (f . a1);
set f2 = (R^1 | (R^1 (right_closed_halfline b))) --> (f . b1);
A3: the carrier of (R^1 | (R^1 (left_closed_halfline a))) = left_closed_halfline a by PRE_TOPC:8;
Closed-Interval-TSpace (a,b) = R^1 | (R^1 [.a,b.]) by A1, TOPMETR:19;
then reconsider f = f as continuous Function of (R^1 | (R^1 [.a,b.])),R^1 ;
A4: dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) = the carrier of (R^1 | (R^1 (left_closed_halfline a)))
.= left_closed_halfline a by PRE_TOPC:8 ;
A5: dom f = the carrier of (R^1 | (R^1 [.a,b.])) by FUNCT_2:def 1
.= [.a,b.] by PRE_TOPC:8 ;
A6: dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) = the carrier of (R^1 | (R^1 (right_closed_halfline b)))
.= right_closed_halfline b by PRE_TOPC:8 ;
b in REAL by XREAL_0:def 1;
then A7: b < +infty by XXREAL_0:9;
(R^1 | (R^1 (left_closed_halfline a))) --> (f . a1) tolerates f
proof
let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) /\ (dom f) or ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) . x = f . x )
assume A8: x in (dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) /\ (dom f) ; :: thesis: ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) . x = f . x
a in REAL by XREAL_0:def 1;
then (left_closed_halfline a) /\ [.a,b.] = {a} by A1, XXREAL_0:12, XXREAL_1:417;
then A9: x = a by A4, A5, A8, TARSKI:def 1;
then a in left_closed_halfline a by A4, A8, XBOOLE_0:def 4;
hence ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) . x = f . x by A3, A9, FUNCOP_1:7; :: thesis: verum
end;
then reconsider ff = ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) +* f as continuous Function of (R^1 | ((R^1 (left_closed_halfline a)) \/ (R^1 [.a,b.]))),R^1 by TOPGEN_5:10;
set G = ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1));
ff tolerates (R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)
proof
let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (dom ff) /\ (dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) or ff . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x )
assume A10: x in (dom ff) /\ (dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) ; :: thesis: ff . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x
then A11: x in dom ff by XBOOLE_0:def 4;
A12: x in dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) by A10;
then reconsider y = x as Real ;
A13: b <= y by A6, A12, XXREAL_1:3;
A14: dom ff = (dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) \/ (dom f) by FUNCT_4:def 1;
per cases ( ( x in dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) & not x in dom f ) or x in dom f ) by A11, A14, XBOOLE_0:def 3;
suppose that A15: x in dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) and
A16: not x in dom f ; :: thesis: ff . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x
y <= a by A4, A15, XXREAL_1:2;
then b <= a by A13, XXREAL_0:2;
then a = b by A1, XXREAL_0:1;
hence ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x = f . a1 by A10, FUNCOP_1:7
.= ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) . x by A15, FUNCOP_1:7
.= ff . x by A16, FUNCT_4:11 ;
:: thesis: verum
end;
suppose A17: x in dom f ; :: thesis: ff . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x
then y <= b by A5, XXREAL_1:1;
then b = y by A13, XXREAL_0:1;
hence ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x = f . x by A10, FUNCOP_1:7
.= ff . x by A17, FUNCT_4:13 ;
:: thesis: verum
end;
end;
end;
then A18: ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) is continuous Function of (R^1 | ((R^1 ((left_closed_halfline a) \/ [.a,b.])) \/ (R^1 (right_closed_halfline b)))),R^1 by TOPGEN_5:10;
A19: ((left_closed_halfline a) \/ [.a,b.]) \/ (right_closed_halfline b) c= REAL ;
A20: dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) = (dom ff) \/ (dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) by FUNCT_4:def 1
.= ((dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) \/ (dom f)) \/ (dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) by FUNCT_4:def 1 ;
A21: dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) = REAL
proof
thus dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) c= REAL by A4, A5, A6, A19, A20; :: according to XBOOLE_0:def 10 :: thesis: REAL c= dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL or x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) )
assume x in REAL ; :: thesis: x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)))
then reconsider y = x as Element of REAL ;
A22: y < +infty by XXREAL_0:9;
A23: -infty < y by XXREAL_0:12;
per cases ( y < b or y >= b ) ;
suppose A24: y < b ; :: thesis: x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)))
end;
end;
end;
then ((left_closed_halfline a) \/ [.a,b.]) \/ (right_closed_halfline b) = [#] R^1 by A4, A5, A6, A20, TOPMETR:17;
then A25: R^1 | ((R^1 ((left_closed_halfline a) \/ [.a,b.])) \/ (R^1 (right_closed_halfline b))) = R^1 by TSEP_1:3;
rng (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) c= REAL by TOPMETR:17;
then reconsider G = ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) as PartFunc of REAL,REAL by A21, RELSET_1:4;
A26: G is continuous by A18, A25, JORDAN5A:7;
A27: dom f = (dom G) /\ [.a,b.] by A5, A21, XBOOLE_1:28;
now :: thesis: for x being object st x in dom f holds
G . x = f . x
let x be object ; :: thesis: ( x in dom f implies G . b1 = f . b1 )
assume A28: x in dom f ; :: thesis: G . b1 = f . b1
then reconsider y = x as Real ;
A29: y <= b by A5, A28, XXREAL_1:1;
per cases ( y < b or y = b ) by A29, XXREAL_0:1;
suppose y < b ; :: thesis: G . b1 = f . b1
then not y in dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) by A6, XXREAL_1:3;
hence G . x = ff . x by FUNCT_4:11
.= f . x by A28, FUNCT_4:13 ;
:: thesis: verum
end;
suppose A30: y = b ; :: thesis: G . b1 = f . b1
then A31: x in dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) by A6, A7, XXREAL_1:3;
hence G . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x by FUNCT_4:13
.= f . x by A30, A31, FUNCOP_1:7 ;
:: thesis: verum
end;
end;
end;
then g = G | [.a,b.] by A2, A27, FUNCT_1:46;
hence g is continuous by A26; :: thesis: verum