let X, Y be non empty TopSpace; 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; for A being Subset of X st f is continuous & A is connected holds
f .: A is connected
let A be Subset of X; ( f is continuous & A is connected implies f .: A is connected )
assume A1:
f is continuous
; ( not A is connected or f .: A is connected )
assume A2:
A is connected
; f .: A is connected
assume
not f .: A is connected
; contradiction
then consider P, Q being Subset of Y such that
A3:
f .: A = P \/ Q
and
A4:
P,Q are_separated
and
A5:
P <> {} Y
and
A6:
Q <> {} Y
by CONNSP_1:15;
reconsider P1 = f " P, Q1 = f " Q as Subset of X ;
set P2 = P1 /\ A;
set Q2 = Q1 /\ A;
set y = the Element of P;
the Element of P in f .: A
by A3, A5, XBOOLE_0:def 3;
then consider x being object such that
A7:
x in dom f
and
A8:
x in A
and
A9:
the Element of P = f . x
by FUNCT_1:def 6;
x in f " P
by A5, A7, A9, FUNCT_1:def 7;
then A10:
P1 /\ A <> {}
by A8, XBOOLE_0:def 4;
A11:
the carrier of X = dom f
by FUNCT_2:def 1;
P misses Cl Q
by A4, CONNSP_1:def 1;
then A12:
( (f " P) /\ (f " (Cl Q)) = f " (P /\ (Cl Q)) & f " (P /\ (Cl Q)) = f " ({} Y) )
by FUNCT_1:68, XBOOLE_0:def 7;
Cl Q1 c= f " (Cl Q)
by A1, Th44;
then
P1 /\ (Cl Q1) = {}
by A12, XBOOLE_1:3, XBOOLE_1:26;
then A13:
P1 misses Cl Q1
by XBOOLE_0:def 7;
Cl P misses Q
by A4, CONNSP_1:def 1;
then A14:
( (f " (Cl P)) /\ (f " Q) = f " ((Cl P) /\ Q) & f " ((Cl P) /\ Q) = f " ({} Y) )
by FUNCT_1:68, XBOOLE_0:def 7;
Cl P1 c= f " (Cl P)
by A1, Th44;
then
(Cl P1) /\ Q1 = {} X
by A14, XBOOLE_1:3, XBOOLE_1:26;
then
Cl P1 misses Q1
by XBOOLE_0:def 7;
then A15:
P1,Q1 are_separated
by A13, CONNSP_1:def 1;
set z = the Element of Q;
the Element of Q in P \/ Q
by A6, XBOOLE_0:def 3;
then consider x1 being object such that
A16:
x1 in dom f
and
A17:
x1 in A
and
A18:
the Element of Q = f . x1
by A3, FUNCT_1:def 6;
x1 in f " Q
by A6, A16, A18, FUNCT_1:def 7;
then A19:
Q1 /\ A <> {}
by A17, XBOOLE_0:def 4;
f " (f .: A) = (f " P) \/ (f " Q)
by A3, RELAT_1:140;
then A20: A =
(P1 \/ Q1) /\ A
by A11, FUNCT_1:76, XBOOLE_1:28
.=
(P1 /\ A) \/ (Q1 /\ A)
by XBOOLE_1:23
;
( P1 /\ A c= P1 & Q1 /\ A c= Q1 )
by XBOOLE_1:17;
then
ex P3, Q3 being Subset of X st
( A = P3 \/ Q3 & P3,Q3 are_separated & P3 <> {} X & Q3 <> {} X )
by A15, A20, A10, A19, CONNSP_1:7;
hence
contradiction
by A2, CONNSP_1:15; verum