let S, T be non empty TopSpace; :: thesis: for f being Function of S,T st f is bijective & ex K being Basis of S ex L being Basis of T st f .: K = L holds

f is being_homeomorphism

let f be Function of S,T; :: thesis: ( f is bijective & ex K being Basis of S ex L being Basis of T st f .: K = L implies f is being_homeomorphism )

assume A1: f is bijective ; :: thesis: ( for K being Basis of S

for L being Basis of T holds not f .: K = L or f is being_homeomorphism )

given K being Basis of S, L being Basis of T such that A2: f .: K = L ; :: thesis: f is being_homeomorphism

for W being Subset of T st W in L holds

f " W is open

for V being Subset of S st V in K holds

f .: V is open

then A5: f " is continuous by A1, TOPREALA:14;

A6: rng f = the carrier of T by A1, FUNCT_2:def 3

.= [#] T by STRUCT_0:def 3 ;

dom f = the carrier of S by FUNCT_2:def 1

.= [#] S by STRUCT_0:def 3 ;

hence f is being_homeomorphism by A1, A5, A4, A6, TOPS_2:def 5; :: thesis: verum

f is being_homeomorphism

let f be Function of S,T; :: thesis: ( f is bijective & ex K being Basis of S ex L being Basis of T st f .: K = L implies f is being_homeomorphism )

assume A1: f is bijective ; :: thesis: ( for K being Basis of S

for L being Basis of T holds not f .: K = L or f is being_homeomorphism )

given K being Basis of S, L being Basis of T such that A2: f .: K = L ; :: thesis: f is being_homeomorphism

for W being Subset of T st W in L holds

f " W is open

proof

then A4:
f is continuous
by YELLOW_9:34;
let W be Subset of T; :: thesis: ( W in L implies f " W is open )

assume W in L ; :: thesis: f " W is open

then consider V being Subset of S such that

A3: ( V in K & W = f .: V ) by A2, FUNCT_2:def 10;

dom f = the carrier of S by FUNCT_2:def 1;

then V = f " W by A1, A3, FUNCT_1:94;

hence f " W is open by A3, TOPS_2:def 1; :: thesis: verum

end;assume W in L ; :: thesis: f " W is open

then consider V being Subset of S such that

A3: ( V in K & W = f .: V ) by A2, FUNCT_2:def 10;

dom f = the carrier of S by FUNCT_2:def 1;

then V = f " W by A1, A3, FUNCT_1:94;

hence f " W is open by A3, TOPS_2:def 1; :: thesis: verum

for V being Subset of S st V in K holds

f .: V is open

proof

then
f is open
by Th45;
let V be Subset of S; :: thesis: ( V in K implies f .: V is open )

assume V in K ; :: thesis: f .: V is open

then f .: V in f .: K by FUNCT_2:def 10;

hence f .: V is open by A2, TOPS_2:def 1; :: thesis: verum

end;assume V in K ; :: thesis: f .: V is open

then f .: V in f .: K by FUNCT_2:def 10;

hence f .: V is open by A2, TOPS_2:def 1; :: thesis: verum

then A5: f " is continuous by A1, TOPREALA:14;

A6: rng f = the carrier of T by A1, FUNCT_2:def 3

.= [#] T by STRUCT_0:def 3 ;

dom f = the carrier of S by FUNCT_2:def 1

.= [#] S by STRUCT_0:def 3 ;

hence f is being_homeomorphism by A1, A5, A4, A6, TOPS_2:def 5; :: thesis: verum