let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y
for A being Subset of X st f is continuous & A is connected holds
f .: A is connected
let f be Function of X,Y; :: thesis: for A being Subset of X st f is continuous & A is connected holds
f .: A is connected
let A be Subset of X; :: thesis: ( f is continuous & A is connected implies f .: A is connected )
assume A1: f is continuous ; :: thesis: ( not A is connected or f .: A is connected )
assume A2: A is connected ; :: thesis: f .: A is connected
assume not f .: A is connected ; :: thesis: contradiction
then consider P, Q being Subset of Y such that
A3: ( f .: A = P \/ Q & P,Q are_separated & P <> {} Y & Q <> {} Y ) by CONNSP_1:16;
A4: ( Cl P misses Q & P misses Cl Q ) by A3, CONNSP_1:def 1;
consider y being Element of P;
y in f .: A by A3, XBOOLE_0:def 3;
then consider x being set such that
A5: ( x in dom f & x in A & y = f . x ) by FUNCT_1:def 12;
A6: x in f " P by A3, A5, FUNCT_1:def 13;
consider z being Element of Q;
z in P \/ Q by A3, XBOOLE_0:def 3;
then consider x1 being set such that
A7: ( x1 in dom f & x1 in A & z = f . x1 ) by A3, FUNCT_1:def 12;
A8: x1 in f " Q by A3, A7, FUNCT_1:def 13;
A9: f " (f .: A) = (f " P) \/ (f " Q) by A3, RELAT_1:175;
A10: the carrier of X = dom f by FUNCT_2:def 1;
reconsider P1 = f " P, Q1 = f " Q as Subset of X ;
A11: Cl P1 c= f " (Cl P) by A1, Th56;
A12: Cl Q1 c= f " (Cl Q) by A1, Th56;
A13: (f " (Cl P)) /\ (f " Q) = f " ((Cl P) /\ Q) by FUNCT_1:137;
A14: f " ((Cl P) /\ Q) = f " ({} Y) by A4, XBOOLE_0:def 7;
A15: (f " P) /\ (f " (Cl Q)) = f " (P /\ (Cl Q)) by FUNCT_1:137;
A16: f " (P /\ (Cl Q)) = f " ({} Y) by A4, XBOOLE_0:def 7;
A17: f " ({} Y) = {} by RELAT_1:171;
then (Cl P1) /\ Q1 = {} X by A11, A13, A14, XBOOLE_1:3, XBOOLE_1:26;
then A18: Cl P1 misses Q1 by XBOOLE_0:def 7;
P1 /\ (Cl Q1) = {} by A12, A15, A16, A17, XBOOLE_1:3, XBOOLE_1:26;
then P1 misses Cl Q1 by XBOOLE_0:def 7;
then A19: P1,Q1 are_separated by A18, CONNSP_1:def 1;
set P2 = P1 /\ A;
set Q2 = Q1 /\ A;
A20: A = (P1 \/ Q1) /\ A by A9, A10, FUNCT_1:146, XBOOLE_1:28
.= (P1 /\ A) \/ (Q1 /\ A) by XBOOLE_1:23 ;
A21: P1 /\ A c= P1 by XBOOLE_1:17;
A22: Q1 /\ A c= Q1 by XBOOLE_1:17;
A23: P1 /\ A <> {} by A5, A6, XBOOLE_0:def 4;
Q1 /\ A <> {} by A7, A8, XBOOLE_0:def 4;
then ex P3, Q3 being Subset of X st
( A = P3 \/ Q3 & P3,Q3 are_separated & P3 <> {} X & Q3 <> {} X ) by A19, A20, A21, A22, A23, CONNSP_1:8;
hence contradiction by A2, CONNSP_1:16; :: thesis: verum