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