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

for n being 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 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 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 that

A1: h is being_homeomorphism and

A2: 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) )

x in the carrier of FT1 ;

then A3: x in dom h by FUNCT_2:def 1;

consider g being Function of FT2,FT1 such that

A4: g = h " and

A5: g is being_homeomorphism by A1, Th3;

( h is one-to-one & h is onto ) by A1;

then x = g . y by A2, A4, A3, FUNCT_1:34;

hence for v being Element of FT2 holds

( (h ") . v in U_FT (x,n) iff v in U_FT (y,n) ) by A4, A5, Th4; :: thesis: verum

for n being 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 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 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 that

A1: h is being_homeomorphism and

A2: 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) )

x in the carrier of FT1 ;

then A3: x in dom h by FUNCT_2:def 1;

consider g being Function of FT2,FT1 such that

A4: g = h " and

A5: g is being_homeomorphism by A1, Th3;

( h is one-to-one & h is onto ) by A1;

then x = g . y by A2, A4, A3, FUNCT_1:34;

hence for v being Element of FT2 holds

( (h ") . v in U_FT (x,n) iff v in U_FT (y,n) ) by A4, A5, Th4; :: thesis: verum