let GX, GY be TopSpace; 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; ( 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
; GY is connected
assume
not GY is connected
; 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 Th11;
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, XBOOLE_0:def 7;
(F " A) /\ (F " B) =
F " (A /\ B)
by FUNCT_1:68
.=
{}
by A12, RELAT_1:136
;
then A13:
F " A misses F " B
by XBOOLE_0:def 7;
A14:
not the carrier of GY is empty
by A5;
then A15: [#] GX =
F " the carrier of GY
by FUNCT_2:40
.=
(F " A) \/ (F " B)
by A4, RELAT_1:140
;
A16:
rng F = F .: the carrier of GX
by A14, FUNCT_2:37;
then A17:
F " B <> {} GX
by A2, A6, RELAT_1:139;
F " A <> {} GX
by A2, A5, A16, RELAT_1:139;
hence
contradiction
by A3, A15, A13, A10, A11, A17, Th11; verum