let T be non empty TopSpace; :: thesis: for f being continuous RealMap of T

for A being Subset of T st A is connected holds

f .: A is interval

let f be continuous RealMap of T; :: thesis: for A being Subset of T st A is connected holds

f .: A is interval

let A be Subset of T; :: thesis: ( A is connected implies f .: A is interval )

assume A1: A is connected ; :: thesis: f .: A is interval

let r, s be ExtReal; :: according to XXREAL_2:def 12 :: thesis: ( not r in f .: A or not s in f .: A or [.r,s.] c= f .: A )

A2: A c= f " (f .: A) by FUNCT_2:42;

assume A3: r in f .: A ; :: thesis: ( not s in f .: A or [.r,s.] c= f .: A )

then consider p being Point of T such that

A4: p in A and

A5: r = f . p by FUNCT_2:65;

assume A6: s in f .: A ; :: thesis: [.r,s.] c= f .: A

then consider q being Point of T such that

A7: q in A and

A8: s = f . q by FUNCT_2:65;

assume A9: not [.r,s.] c= f .: A ; :: thesis: contradiction

reconsider r = r, s = s as Real by A3, A6;

consider t being Element of REAL such that

A10: t in [.r,s.] and

A11: not t in f .: A by A9;

reconsider r = r, s = s, t = t as Real ;

set P1 = f " (left_open_halfline t);

set Q1 = f " (right_open_halfline t);

set P = (f " (left_open_halfline t)) /\ A;

set Q = (f " (right_open_halfline t)) /\ A;

set X = (left_open_halfline t) \/ (right_open_halfline t);

A12: f " (right_open_halfline t) is open by PSCOMP_1:8;

t <= s by A10, XXREAL_1:1;

then A13: t < s by A6, A11, XXREAL_0:1;

right_open_halfline t = { r1 where r1 is Real : t < r1 } by XXREAL_1:230;

then s in right_open_halfline t by A13;

then q in f " (right_open_halfline t) by A8, FUNCT_2:38;

then A14: (f " (right_open_halfline t)) /\ A <> {} T by A7, XBOOLE_0:def 4;

(left_open_halfline t) /\ (right_open_halfline t) = ].t,t.[ by XXREAL_1:269

.= {} by XXREAL_1:28 ;

then left_open_halfline t misses right_open_halfline t ;

then f " (left_open_halfline t) misses f " (right_open_halfline t) by FUNCT_1:71;

then (f " (left_open_halfline t)) /\ (f " (right_open_halfline t)) = {} ;

then A15: (f " (left_open_halfline t)) /\ (f " (right_open_halfline t)) misses ((f " (left_open_halfline t)) /\ A) \/ ((f " (right_open_halfline t)) /\ A) ;

reconsider Y = {t} as Subset of REAL ;

Y ` = REAL \ [.t,t.] by XXREAL_1:17

.= (left_open_halfline t) \/ (right_open_halfline t) by XXREAL_1:385 ;

then A16: (f " Y) ` = f " ((left_open_halfline t) \/ (right_open_halfline t)) by FUNCT_2:100

.= (f " (left_open_halfline t)) \/ (f " (right_open_halfline t)) by RELAT_1:140 ;

f " {t} misses f " (f .: A) by A11, FUNCT_1:71, ZFMISC_1:50;

then f " {t} misses A by A2, XBOOLE_1:63;

then A c= (f " (left_open_halfline t)) \/ (f " (right_open_halfline t)) by A16, SUBSET_1:23;

then A17: A = A /\ ((f " (left_open_halfline t)) \/ (f " (right_open_halfline t))) by XBOOLE_1:28

.= ((f " (left_open_halfline t)) /\ A) \/ ((f " (right_open_halfline t)) /\ A) by XBOOLE_1:23 ;

A18: (f " (left_open_halfline t)) /\ A c= f " (left_open_halfline t) by XBOOLE_1:17;

r <= t by A10, XXREAL_1:1;

then A19: r < t by A3, A11, XXREAL_0:1;

left_open_halfline t = { r1 where r1 is Real : r1 < t } by XXREAL_1:229;

then r in left_open_halfline t by A19;

then p in f " (left_open_halfline t) by A5, FUNCT_2:38;

then A20: (f " (left_open_halfline t)) /\ A <> {} T by A4, XBOOLE_0:def 4;

A21: (f " (right_open_halfline t)) /\ A c= f " (right_open_halfline t) by XBOOLE_1:17;

f " (left_open_halfline t) is open by PSCOMP_1:8;

then (f " (left_open_halfline t)) /\ A,(f " (right_open_halfline t)) /\ A are_separated by A12, A18, A21, A15, TSEP_1:45;

hence contradiction by A1, A17, A20, A14, CONNSP_1:15; :: thesis: verum

for A being Subset of T st A is connected holds

f .: A is interval

let f be continuous RealMap of T; :: thesis: for A being Subset of T st A is connected holds

f .: A is interval

let A be Subset of T; :: thesis: ( A is connected implies f .: A is interval )

assume A1: A is connected ; :: thesis: f .: A is interval

let r, s be ExtReal; :: according to XXREAL_2:def 12 :: thesis: ( not r in f .: A or not s in f .: A or [.r,s.] c= f .: A )

A2: A c= f " (f .: A) by FUNCT_2:42;

assume A3: r in f .: A ; :: thesis: ( not s in f .: A or [.r,s.] c= f .: A )

then consider p being Point of T such that

A4: p in A and

A5: r = f . p by FUNCT_2:65;

assume A6: s in f .: A ; :: thesis: [.r,s.] c= f .: A

then consider q being Point of T such that

A7: q in A and

A8: s = f . q by FUNCT_2:65;

assume A9: not [.r,s.] c= f .: A ; :: thesis: contradiction

reconsider r = r, s = s as Real by A3, A6;

consider t being Element of REAL such that

A10: t in [.r,s.] and

A11: not t in f .: A by A9;

reconsider r = r, s = s, t = t as Real ;

set P1 = f " (left_open_halfline t);

set Q1 = f " (right_open_halfline t);

set P = (f " (left_open_halfline t)) /\ A;

set Q = (f " (right_open_halfline t)) /\ A;

set X = (left_open_halfline t) \/ (right_open_halfline t);

A12: f " (right_open_halfline t) is open by PSCOMP_1:8;

t <= s by A10, XXREAL_1:1;

then A13: t < s by A6, A11, XXREAL_0:1;

right_open_halfline t = { r1 where r1 is Real : t < r1 } by XXREAL_1:230;

then s in right_open_halfline t by A13;

then q in f " (right_open_halfline t) by A8, FUNCT_2:38;

then A14: (f " (right_open_halfline t)) /\ A <> {} T by A7, XBOOLE_0:def 4;

(left_open_halfline t) /\ (right_open_halfline t) = ].t,t.[ by XXREAL_1:269

.= {} by XXREAL_1:28 ;

then left_open_halfline t misses right_open_halfline t ;

then f " (left_open_halfline t) misses f " (right_open_halfline t) by FUNCT_1:71;

then (f " (left_open_halfline t)) /\ (f " (right_open_halfline t)) = {} ;

then A15: (f " (left_open_halfline t)) /\ (f " (right_open_halfline t)) misses ((f " (left_open_halfline t)) /\ A) \/ ((f " (right_open_halfline t)) /\ A) ;

reconsider Y = {t} as Subset of REAL ;

Y ` = REAL \ [.t,t.] by XXREAL_1:17

.= (left_open_halfline t) \/ (right_open_halfline t) by XXREAL_1:385 ;

then A16: (f " Y) ` = f " ((left_open_halfline t) \/ (right_open_halfline t)) by FUNCT_2:100

.= (f " (left_open_halfline t)) \/ (f " (right_open_halfline t)) by RELAT_1:140 ;

f " {t} misses f " (f .: A) by A11, FUNCT_1:71, ZFMISC_1:50;

then f " {t} misses A by A2, XBOOLE_1:63;

then A c= (f " (left_open_halfline t)) \/ (f " (right_open_halfline t)) by A16, SUBSET_1:23;

then A17: A = A /\ ((f " (left_open_halfline t)) \/ (f " (right_open_halfline t))) by XBOOLE_1:28

.= ((f " (left_open_halfline t)) /\ A) \/ ((f " (right_open_halfline t)) /\ A) by XBOOLE_1:23 ;

A18: (f " (left_open_halfline t)) /\ A c= f " (left_open_halfline t) by XBOOLE_1:17;

r <= t by A10, XXREAL_1:1;

then A19: r < t by A3, A11, XXREAL_0:1;

left_open_halfline t = { r1 where r1 is Real : r1 < t } by XXREAL_1:229;

then r in left_open_halfline t by A19;

then p in f " (left_open_halfline t) by A5, FUNCT_2:38;

then A20: (f " (left_open_halfline t)) /\ A <> {} T by A4, XBOOLE_0:def 4;

A21: (f " (right_open_halfline t)) /\ A c= f " (right_open_halfline t) by XBOOLE_1:17;

f " (left_open_halfline t) is open by PSCOMP_1:8;

then (f " (left_open_halfline t)) /\ A,(f " (right_open_halfline t)) /\ A are_separated by A12, A18, A21, A15, TSEP_1:45;

hence contradiction by A1, A17, A20, A14, CONNSP_1:15; :: thesis: verum