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_{1} being Element of bool the carrier of (S | (f " B)) holds

( not b_{1} is connected or not Y c= b_{1} or Y = b_{1} )

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

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

( not 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