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 holds
f .: A is a_component
let f be Function of T1,T2; :: thesis: ( f is being_homeomorphism implies for A being Subset of T1 st A is a_component holds
f .: A is a_component )
assume A1: f is being_homeomorphism ; :: thesis: for A being Subset of T1 st A is a_component holds
f .: A is a_component
let A be Subset of T1; :: thesis: ( A is a_component implies f .: A is a_component )
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
thus f .: A is connected by A1, A2, TOPS_2:61; :: according to CONNSP_1:def 5 :: thesis: for b₁ being Element of K16( 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 )
rng f = the carrier of T2 by A1;
then A4: f .: (f " B) = B by FUNCT_1:77;
A5: f " (f .: A) = A by A1, FUNCT_1:94;
assume that
A6: B is connected and
A7: f .: A c= B ; :: thesis: f .: A = B
f " B is connected by A1, A6, TOPS_2:62;
hence f .: A = B by A3, A4, A5, A7, RELAT_1:143; :: thesis: verum