let T1, T2 be non empty TopSpace; for f being Function of T1,T2 st f is being_homeomorphism holds
for A being Subset of T1 st A is a_component holds
f .: A is a_component
let f be Function of T1,T2; ( f is being_homeomorphism implies for A being Subset of T1 st A is a_component holds
f .: A is a_component )
assume A1:
f is being_homeomorphism
; for A being Subset of T1 st A is a_component holds
f .: A is a_component
let A be Subset of T1; ( A is a_component implies f .: A is a_component )
assume that
A2:
A is connected
and
A3:
for B being Subset of T1 st B is connected & A c= B holds
A = B
; CONNSP_1:def 5 f .: A is a_component
thus
f .: A is connected
by A1, A2, TOPS_2:61; CONNSP_1:def 5 for b1 being Element of K16( the carrier of T2) holds
( not b1 is connected or not f .: A c= b1 or f .: A = b1 )
let B be Subset of T2; ( not B is connected or not f .: A c= B or f .: A = B )
rng f = the carrier of T2
by A1;
then A4:
f .: (f " B) = B
by FUNCT_1:77;
A5:
f " (f .: A) = A
by A1, FUNCT_1:94;
assume that
A6:
B is connected
and
A7:
f .: A c= B
; f .: A = B
f " B is connected
by A1, A6, TOPS_2:62;
hence
f .: A = B
by A3, A4, A5, A7, RELAT_1:143; verum