let FT1, FT2 be non empty RelStr ; :: thesis: for h being Function of FT1,FT2 st h is being_homeomorphism holds

ex g being Function of FT2,FT1 st

( g = h " & g is being_homeomorphism )

let h be Function of FT1,FT2; :: thesis: ( h is being_homeomorphism implies ex g being Function of FT2,FT1 st

( g = h " & g is being_homeomorphism ) )

assume A1: h is being_homeomorphism ; :: thesis: ex g being Function of FT2,FT1 st

( g = h " & g is being_homeomorphism )

then A2: ( h is one-to-one & h is onto ) ;

then A3: rng h = the carrier of FT2 by FUNCT_2:def 3;

then reconsider g2 = h " as Function of FT2,FT1 by A2, FUNCT_2:25;

A4: for y being Element of FT2 holds g2 .: (U_FT y) = Im ( the InternalRel of FT1,(g2 . y))

.= the carrier of FT1 by FUNCT_2:def 1 ;

then A5: g2 is onto by FUNCT_2:def 3;

g2 is one-to-one by A2, FUNCT_1:40;

then g2 is being_homeomorphism by A5, A4;

hence ex g being Function of FT2,FT1 st

( g = h " & g is being_homeomorphism ) ; :: thesis: verum

ex g being Function of FT2,FT1 st

( g = h " & g is being_homeomorphism )

let h be Function of FT1,FT2; :: thesis: ( h is being_homeomorphism implies ex g being Function of FT2,FT1 st

( g = h " & g is being_homeomorphism ) )

assume A1: h is being_homeomorphism ; :: thesis: ex g being Function of FT2,FT1 st

( g = h " & g is being_homeomorphism )

then A2: ( h is one-to-one & h is onto ) ;

then A3: rng h = the carrier of FT2 by FUNCT_2:def 3;

then reconsider g2 = h " as Function of FT2,FT1 by A2, FUNCT_2:25;

A4: for y being Element of FT2 holds g2 .: (U_FT y) = Im ( the InternalRel of FT1,(g2 . y))

proof

rng g2 =
dom h
by A2, FUNCT_1:33
let y be Element of FT2; :: thesis: g2 .: (U_FT y) = Im ( the InternalRel of FT1,(g2 . y))

reconsider x = g2 . y as Element of FT1 ;

( y = h . x & h .: (U_FT x) = Im ( the InternalRel of FT2,(h . x)) ) by A1, A3, FUNCT_1:35;

hence g2 .: (U_FT y) = Im ( the InternalRel of FT1,(g2 . y)) by A2, Th1; :: thesis: verum

end;reconsider x = g2 . y as Element of FT1 ;

( y = h . x & h .: (U_FT x) = Im ( the InternalRel of FT2,(h . x)) ) by A1, A3, FUNCT_1:35;

hence g2 .: (U_FT y) = Im ( the InternalRel of FT1,(g2 . y)) by A2, Th1; :: thesis: verum

.= the carrier of FT1 by FUNCT_2:def 1 ;

then A5: g2 is onto by FUNCT_2:def 3;

g2 is one-to-one by A2, FUNCT_1:40;

then g2 is being_homeomorphism by A5, A4;

hence ex g being Function of FT2,FT1 st

( g = h " & g is being_homeomorphism ) ; :: thesis: verum