let GX, GY be TopSpace; :: thesis: for F being Function of GX,GY st F is continuous & F .: ([#] GX) = [#] GY & GX is connected holds
GY is connected
let F be Function of GX,GY; :: thesis: ( F is continuous & F .: ([#] GX) = [#] GY & GX is connected implies GY is connected )
assume that
A1: F is continuous and
A2: F .: ([#] GX) = [#] GY and
A3: GX is connected ; :: thesis: GY is connected
assume not GY is connected ; :: thesis: contradiction
then consider A, B being Subset of GY such that
A4: [#] GY = A \/ B and
A5: ( A <> {} GY & B <> {} GY ) and
A6: ( A is closed & B is closed ) and
A7: A misses B by Th11;
A8: A /\ B = {} by A7, XBOOLE_0:def 7;
A9: not the carrier of GY is empty by A5;
then A10: [#] GX = F " the carrier of GY by FUNCT_2:48
.= (F " A) \/ (F " B) by A4, RELAT_1:175 ;
(F " A) /\ (F " B) = F " (A /\ B) by FUNCT_1:137
.= {} by A8, RELAT_1:171 ;
then A11: F " A misses F " B by XBOOLE_0:def 7;
A12: ( F " A is closed & F " B is closed ) by A1, A6, PRE_TOPC:def 12;
rng F = F .: the carrier of GX by A9, FUNCT_2:45;
then ( F " A <> {} GX & F " B <> {} GX ) by A2, A5, RELAT_1:174;
hence contradiction by A3, A10, A11, A12, Th11; :: thesis: verum