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))
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 A1, A3, FUNCT_1:35;
hence g2 .: (U_FT y) = Im ( the InternalRel of FT1,(g2 . y)) by A2, Th1; :: thesis: verum
end;
rng g2 = dom h by A2, FUNCT_1:33
.= 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