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 A1, A7, PRE_TOPC:def 6;

A11: F " B is closed by A1, A8, PRE_TOPC:def 6;

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 A4, RELAT_1:140 ;

A15: rng F = F .: the carrier of GX by RELSET_1:22;

then A16: F " B <> {} GX by A2, A6, RELAT_1:139;

F " A <> {} GX by A2, A5, A15, RELAT_1:139;

hence contradiction by A3, A14, A13, A10, A11, A16, Th10; :: thesis: verum

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 A1, A7, PRE_TOPC:def 6;

A11: F " B is closed by A1, A8, PRE_TOPC:def 6;

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 A4, RELAT_1:140 ;

A15: rng F = F .: the carrier of GX by RELSET_1:22;

then A16: F " B <> {} GX by A2, A6, RELAT_1:139;

F " A <> {} GX by A2, A5, A15, RELAT_1:139;

hence contradiction by A3, A14, A13, A10, A11, A16, Th10; :: thesis: verum