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