let X, Y be non empty TopStruct ; :: thesis: for f being Function of X,Y
for g being Function of Y,X st f = id X & g = id X & f is continuous & g is continuous holds
TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #)
let f be Function of X,Y; :: thesis: for g being Function of Y,X st f = id X & g = id X & f is continuous & g is continuous holds
TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #)
let g be Function of Y,X; :: thesis: ( f = id X & g = id X & f is continuous & g is continuous implies TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) )
assume that
A1: f = id X and
A2: g = id X and
A3: f is continuous and
A4: g is continuous ; :: thesis: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #)
A5: the carrier of X = dom f by FUNCT_2:def 1
.= the carrier of Y by A2, FUNCT_2:def 1 ;
A6: [#] Y <> {} ;
A7: [#] X <> {} ;
the topology of X = the topology of Y
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the topology of Y c= the topology of X
let A be object ; :: thesis: ( A in the topology of X implies A in the topology of Y )
assume A8: A in the topology of X ; :: thesis: A in the topology of Y
then reconsider B = A as Subset of X ;
B is open by A8;
then A9: g " B is open by A4, A7, TOPS_2:43;
g " B = B by A2, FUNCT_2:94;
hence A in the topology of Y by A9; :: thesis: verum
end;
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in the topology of Y or A in the topology of X )
assume A10: A in the topology of Y ; :: thesis: A in the topology of X
then reconsider B = A as Subset of Y ;
B is open by A10;
then A11: f " B is open by A3, A6, TOPS_2:43;
f " B = B by A1, A5, FUNCT_2:94;
hence A in the topology of X by A11; :: thesis: verum
end;
hence TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) by A5; :: thesis: verum