let S, T be non empty TopSpace; :: thesis: ( S,T are_homeomorphic & S is locally_connected implies T is locally_connected )

given f being Function of S,T such that A1: f is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: ( not S is locally_connected or T is locally_connected )

assume A2: S is locally_connected ; :: thesis: T is locally_connected

given f being Function of S,T such that A1: f is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: ( not S is locally_connected or T is locally_connected )

assume A2: S is locally_connected ; :: thesis: T is locally_connected

now :: thesis: for A being non empty Subset of T

for B being Subset of T st A is open & B is_a_component_of A holds

B is open

hence
T is locally_connected
by CONNSP_2:18; :: thesis: verumfor B being Subset of T st A is open & B is_a_component_of A holds

B is open

let A be non empty Subset of T; :: thesis: for B being Subset of T st A is open & B is_a_component_of A holds

B is open

let B be Subset of T; :: thesis: ( A is open & B is_a_component_of A implies B is open )

assume ( A is open & B is_a_component_of A ) ; :: thesis: B is open

then A3: ( f " A is open & f " B is_a_component_of f " A ) by A1, Th10, TOPGRP_1:26;

rng f = [#] T by A1;

then not f " A is empty by RELAT_1:139;

then f " B is open by A2, A3, CONNSP_2:18;

hence B is open by A1, TOPGRP_1:26; :: thesis: verum

end;B is open

let B be Subset of T; :: thesis: ( A is open & B is_a_component_of A implies B is open )

assume ( A is open & B is_a_component_of A ) ; :: thesis: B is open

then A3: ( f " A is open & f " B is_a_component_of f " A ) by A1, Th10, TOPGRP_1:26;

rng f = [#] T by A1;

then not f " A is empty by RELAT_1:139;

then f " B is open by A2, A3, CONNSP_2:18;

hence B is open by A1, TOPGRP_1:26; :: thesis: verum