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, TOPS_2:def 5
.= 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_of T | B ; :: 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:29;
then f " X c= f " B by RELAT_1:178;
then reconsider Y = f " A as Subset of (S | (f " B)) by A3, PRE_TOPC:29;
take Y ; :: according to CONNSP_1:def 6 :: thesis: ( Y = f " A & Y is_a_component_of S | (f " B) )
thus Y = f " A ; :: thesis: Y is_a_component_of S | (f " B)
X is connected by A4, CONNSP_1:def 5;
then A is connected by A3, CONNSP_1:24;
then f " A is connected by A1, TOPS_2:76;
hence Y is connected by CONNSP_1:24; :: 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:156;
A9: f is one-to-one by A1, TOPS_2:def 5;
A10: f is continuous by A1, TOPS_2:def 5;
the carrier of (S | (f " B)) = f " B by PRE_TOPC:29;
then f .: Z c= f .: (f " B) by RELAT_1:156;
then reconsider R = f .: Z as Subset of (T | B) by A5, A2, FUNCT_1:147;
reconsider Z1 = Z as Subset of S by PRE_TOPC:39;
dom f = the carrier of S by FUNCT_2:def 1;
then A11: Z1 c= dom f ;
Z1 is connected by A6, CONNSP_1:24;
then f .: Z1 is connected by A10, TOPS_2:75;
then A12: R is connected by CONNSP_1:24;
X = f .: Y by A3, A2, FUNCT_1:147;
then X = R by A4, A12, A8, CONNSP_1:def 5;
hence Y = Z by A3, A9, A11, FUNCT_1:164; :: thesis: verum