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 and
A3: A1 is a_component ; :: according to CONNSP_1:def 6 :: thesis: f .: A is_a_component_of f .: B
A4: [#] (T2 | (f .: B)) = f .: B by PRE_TOPC:def 5;
A5: dom f = the carrier of T1 by FUNCT_2:def 1;
A6: [#] (T1 | B) = B by PRE_TOPC:def 5;
then reconsider A2 = f .: A as Subset of (T2 | (f .: B)) by A2, A4, RELAT_1:123;
per cases ( B is empty or not B is empty ) ;
suppose A7: B is empty ; :: thesis: f .: A is_a_component_of f .: B
then f .: B = {} ;
then A8: A2 = {} by A4, XBOOLE_1:3;
{} T2 = f .: B by A7;
hence f .: A is_a_component_of f .: B by A8, JORDAN1K:6; :: thesis: verum
end;
suppose 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 A5;
take A2 ; :: according to CONNSP_1:def 6 :: thesis: ( A2 = f .: A & A2 is a_component )
thus A2 = f .: A ; :: thesis: A2 is a_component
reconsider fB = f | B as Function of S1,S2 by Th12;
fB .: A = A2 by A2, A6, RELAT_1:129;
hence A2 is a_component by A1, A2, A3, Th11, Th14; :: thesis: verum
end;
end;