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 and
A6: B <> {} GY and
A7: A is closed and
A8: B is closed and
A9: A misses B by Th10;
A10: F " A is closed by ;
A11: F " B is closed by ;
A12: A /\ B = {} by A9;
(F " A) /\ (F " B) = F " (A /\ B) by FUNCT_1:68
.= {} by A12 ;
then A13: F " A misses F " B ;
not the carrier of GY is empty by A5;
then A14: [#] GX = F " the carrier of GY by FUNCT_2:40
.= (F " A) \/ (F " B) by ;
A15: rng F = F .: the carrier of GX by RELSET_1:22;
then A16: F " B <> {} GX by ;
F " A <> {} GX by ;
hence contradiction by A3, A14, A13, A10, A11, A16, Th10; :: thesis: verum