let S, T be non empty TopSpace; :: thesis: for A, B being Subset of T
for f being Function of S,T st f is being_homeomorphism & A is_a_component_of B holds
f " A is_a_component_of f " B
let A, B be Subset of T; :: thesis: for f being Function of S,T st f is being_homeomorphism & A is_a_component_of B holds
f " A is_a_component_of f " B
let f be Function of S,T; :: thesis: ( f is being_homeomorphism & A is_a_component_of B implies f " A is_a_component_of f " B )
assume A1: f is being_homeomorphism ; :: thesis: ( not A is_a_component_of B or f " A is_a_component_of f " B )
A2: rng f = [#] T by A1
.= the carrier of T ;
set Y = f " A;
given X being Subset of (T | B) such that A3: X = A and
A4: X is a_component ; :: according to CONNSP_1:def 6 :: thesis: f " A is_a_component_of f " B
A5: the carrier of (T | B) = B by PRE_TOPC:8;
then f " X c= f " B by RELAT_1:143;
then reconsider Y = f " A as Subset of (S | (f " B)) by A3, PRE_TOPC:8;
take Y ; :: according to CONNSP_1:def 6 :: thesis: ( Y = f " A & Y is a_component )
thus Y = f " A ; :: thesis: Y is a_component
X is connected by A4;
then A is connected by A3, CONNSP_1:23;
then f " A is connected by A1, TOPS_2:62;
hence Y is connected by CONNSP_1:23; :: according to CONNSP_1:def 5 :: thesis: for b₁ being Element of bool the carrier of (S | (f " B)) holds
( not b₁ is connected or not Y c= b₁ or Y = b₁ )
let Z be Subset of (S | (f " B)); :: thesis: ( not Z is connected or not Y c= Z or Y = Z )
assume that
A6: Z is connected and
A7: Y c= Z ; :: thesis: Y = Z
A8: f .: Y c= f .: Z by A7, RELAT_1:123;
A9: f is one-to-one by A1;
A10: f is continuous by A1;
the carrier of (S | (f " B)) = f " B by PRE_TOPC:8;
then f .: Z c= f .: (f " B) by RELAT_1:123;
then reconsider R = f .: Z as Subset of (T | B) by A5, A2, FUNCT_1:77;
reconsider Z1 = Z as Subset of S by PRE_TOPC:11;
dom f = the carrier of S by FUNCT_2:def 1;
then A11: Z1 c= dom f ;
Z1 is connected by A6, CONNSP_1:23;
then f .: Z1 is connected by A10, TOPS_2:61;
then A12: R is connected by CONNSP_1:23;
X = f .: Y by A3, A2, FUNCT_1:77;
then X = R by A4, A12, A8;
hence Y = Z by A3, A9, A11, FUNCT_1:94; :: thesis: verum