let FT1, FT2 be non empty RelStr ; :: thesis: for h being Function of FT1,FT2
for n being Element of NAT
for x being Element of FT1
for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for v being Element of FT2 holds
( (h " ) . v in U_FT x,n iff v in U_FT y,n )
let h be Function of FT1,FT2; :: thesis: for n being Element of NAT
for x being Element of FT1
for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for v being Element of FT2 holds
( (h " ) . v in U_FT x,n iff v in U_FT y,n )
let n be Element of NAT ; :: thesis: for x being Element of FT1
for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for v being Element of FT2 holds
( (h " ) . v in U_FT x,n iff v in U_FT y,n )
let x be Element of FT1; :: thesis: for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for v being Element of FT2 holds
( (h " ) . v in U_FT x,n iff v in U_FT y,n )
let y be Element of FT2; :: thesis: ( h is being_homeomorphism & y = h . x implies for v being Element of FT2 holds
( (h " ) . v in U_FT x,n iff v in U_FT y,n ) )
assume A1: ( h is being_homeomorphism & y = h . x ) ; :: thesis: for v being Element of FT2 holds
( (h " ) . v in U_FT x,n iff v in U_FT y,n )
then consider g being Function of FT2,FT1 such that
A2: ( g = h " & g is being_homeomorphism ) by Th3;
x in the carrier of FT1 ;
then A3: x in dom h by FUNCT_2:def 1;
( h is one-to-one & h is onto & ( for x2 being Element of FT1 holds h .: (U_FT x2) = Im the InternalRel of FT2,(h . x2) ) ) by A1, Def1;
then x = g . y by A1, A2, A3, FUNCT_1:56;
hence for v being Element of FT2 holds
( (h " ) . v in U_FT x,n iff v in U_FT y,n ) by A2, Th4; :: thesis: verum