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 & ( for x being Element of FT1 holds h .: (U_FT x) = Im the InternalRel of FT2,(h . x) ) ) by Def1;
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:31;
A4: g2 is one-to-one by A2, FUNCT_1:62;
rng g2 = dom h by A2, FUNCT_1:55
.= the carrier of FT1 by FUNCT_2:def 1 ;
then A5: g2 is onto by FUNCT_2:def 3;
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 ;
A6: y = h . x by A2, A3, FUNCT_1:57;
h .: (U_FT x) = Im the InternalRel of FT2,(h . x) by A1, Def1;
hence g2 .: (U_FT y) = Im the InternalRel of FT1,(g2 . y) by A2, A6, Th1; :: thesis: verum

end;

then g2 is being_homeomorphism by A4, A5, Def1;
hence ex g being Function of FT2,FT1 st
( g = h " & g is being_homeomorphism ) ; :: thesis: verum