let T1, T2 be non empty TopSpace; :: thesis: for f being Function of T1,T2 st f is being_homeomorphism holds
for A being Subset of T1 st A is_a_component_of T1 holds
f .: A is_a_component_of T2
let f be Function of T1,T2; :: thesis: ( f is being_homeomorphism implies for A being Subset of T1 st A is_a_component_of T1 holds
f .: A is_a_component_of T2 )
assume A1: f is being_homeomorphism ; :: thesis: for A being Subset of T1 st A is_a_component_of T1 holds
f .: A is_a_component_of T2
let A be Subset of T1; :: thesis: ( A is_a_component_of T1 implies f .: A is_a_component_of T2 )
assume that
A2: A is connected and
A3: for B being Subset of T1 st B is connected & A c= B holds
A = B ; :: according to CONNSP_1:def 5 :: thesis: f .: A is_a_component_of T2
thus f .: A is connected by A1, A2, TOPS_2:75; :: according to CONNSP_1:def 5 :: thesis: for b₁ being Element of K24(the carrier of T2) holds
( not b₁ is connected or not f .: A c= b₁ or f .: A = b₁ )
let B be Subset of T2; :: thesis: ( not B is connected or not f .: A c= B or f .: A = B )
[#] T2 = the carrier of T2 ;
then ( f is one-to-one & rng f = the carrier of T2 & dom f = the carrier of T1 ) by A1, FUNCT_2:def 1, TOPS_2:def 5;
then A4: ( f .: (f " B) = B & f " (f .: A) = A ) by FUNCT_1:147, FUNCT_1:164;
assume ( B is connected & f .: A c= B ) ; :: thesis: f .: A = B
then ( f " B is connected & A c= f " B ) by A1, A4, RELAT_1:178, TOPS_2:76;
hence f .: A = B by A3, A4; :: thesis: verum