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 ;
A4: for y being Element of FT2 holds g2 .: (U_FT y) = Im ( the InternalRel of FT1,(g2 . y))
proof
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 ;
hence g2 .: (U_FT y) = Im ( the InternalRel of FT1,(g2 . y)) by ; :: thesis: verum
end;
rng g2 = dom h by
.= 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 ;
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