let T1, T2 be non empty TopSpace; :: thesis: for f being Function of T1,T2 st f is being_homeomorphism holds
for A, B being Subset of T1 st A is_a_component_of B holds
f .: A is_a_component_of f .: B
let f be Function of T1,T2; :: thesis: ( f is being_homeomorphism implies for A, B being Subset of T1 st A is_a_component_of B holds
f .: A is_a_component_of f .: B )
assume A1: f is being_homeomorphism ; :: thesis: for A, B being Subset of T1 st A is_a_component_of B holds
f .: A is_a_component_of f .: B
let A, B be Subset of T1; :: thesis: ( A is_a_component_of B implies f .: A is_a_component_of f .: B )
given A1 being Subset of (T1 | B) such that A2: ( A1 = A & A1 is_a_component_of T1 | B ) ; :: according to CONNSP_1:def 6 :: thesis: f .: A is_a_component_of f .: B
A3: ( [#] (T1 | B) = B & [#] (T2 | (f .: B)) = f .: B ) by PRE_TOPC:def 10;
then reconsider A2 = f .: A as Subset of (T2 | (f .: B)) by A2, RELAT_1:156;
A4: dom f = the carrier of T1 by FUNCT_2:def 1;

per cases ( B is empty or not B is empty ) ;

suppose B is empty ; :: thesis: f .: A is_a_component_of f .: B

then f .: B = {} by RELAT_1:149;
then ( A2 = {} & {} T2 = f .: B ) by A3, XBOOLE_1:3;
hence f .: A is_a_component_of f .: B by JORDAN1K:6; :: thesis: verum

end;

suppose A5: not B is empty ; :: thesis: f .: A is_a_component_of f .: B

then reconsider S1 = T1 | B, S2 = T2 | (f .: B) as non empty TopSpace by A4;
take A2 ; :: according to CONNSP_1:def 6 :: thesis: ( A2 = f .: A & A2 is_a_component_of T2 | (f .: B) )
thus A2 = f .: A ; :: thesis: A2 is_a_component_of T2 | (f .: B)
reconsider fB = f | B as Function of S1,S2 by Th12;
( fB .: A = A2 & fB is being_homeomorphism ) by A1, A2, A3, Th14, RELAT_1:162;
hence A2 is_a_component_of T2 | (f .: B) by A2, Th11; :: thesis: verum

end;

end;