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 z being Element of FT1 holds
( z in U_FT (x,n) iff h . z 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 z being Element of FT1 holds
( z in U_FT (x,n) iff h . z 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 z being Element of FT1 holds
( z in U_FT (x,n) iff h . z 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 z being Element of FT1 holds
( z in U_FT (x,n) iff h . z in U_FT (y,n) )
let y be Element of FT2; :: thesis: ( h is being_homeomorphism & y = h . x implies for z being Element of FT1 holds
( z in U_FT (x,n) iff h . z in U_FT (y,n) ) )
assume that
A1: h is being_homeomorphism and
A2: y = h . x ; :: thesis: for z being Element of FT1 holds
( z in U_FT (x,n) iff h . z in U_FT (y,n) )
A3: ( h is one-to-one & h is onto ) by A1;
let z be Element of FT1; :: thesis: ( z in U_FT (x,n) iff h . z in U_FT (y,n) )
x in the carrier of FT1 ;
then A4: x in dom h by FUNCT_2:def 1;
z in the carrier of FT1 ;
then A5: z in dom h by FUNCT_2:def 1;

A6: now :: thesis: ( h . z in U_FT (y,n) implies z in U_FT (x,n) )

defpred S₁[ Nat] means for w being Element of FT2 st w in U_FT (y,$1) holds
(h ") . w in U_FT (x,$1);
assume A7: h . z in U_FT (y,n) ; :: thesis: z in U_FT (x,n)
consider g being Function of FT2,FT1 such that
A8: g = h " and
A9: g is being_homeomorphism by A1, Th3;
A10: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A11: S₁[k] ; :: thesis: S₁[k + 1]
for w being Element of FT2 st w in U_FT (y,(k + 1)) holds
(h ") . w in U_FT (x,(k + 1))

proof

let w be Element of FT2; :: thesis: ( w in U_FT (y,(k + 1)) implies (h ") . w in U_FT (x,(k + 1)) )
A12: U_FT (y,(k + 1)) = (U_FT (y,k)) ^f by FINTOPO3:48;
assume w in U_FT (y,(k + 1)) ; :: thesis: (h ") . w in U_FT (x,(k + 1))
then consider x3 being Element of FT2 such that
A13: x3 = w and
A14: ex y3 being Element of FT2 st
( y3 in U_FT (y,k) & x3 in U_FT y3 ) by A12;
consider y2 being Element of FT2 such that
A15: y2 in U_FT (y,k) and
A16: x3 in U_FT y2 by A14;
reconsider q = g . y2, p = g . x3 as Element of FT1 ;
A17: for w2 being Element of FT2 st w2 in U_FT (y2,0) holds
(h ") . w2 in U_FT (q,0)

proof

let w2 be Element of FT2; :: thesis: ( w2 in U_FT (y2,0) implies (h ") . w2 in U_FT (q,0) )
w2 in the carrier of FT2 ;
then A18: w2 in dom g by FUNCT_2:def 1;
A19: (h ") .: (U_FT y2) = Class ( the InternalRel of FT1,((h ") . y2)) by A8, A9;

hereby :: thesis: verum

assume w2 in U_FT (y2,0) ; :: thesis: (h ") . w2 in U_FT (q,0)
then w2 in U_FT y2 by FINTOPO3:47;
then (h ") . w2 in U_FT q by A8, A19, A18, FUNCT_1:def 6;
hence (h ") . w2 in U_FT (q,0) by FINTOPO3:47; :: thesis: verum

end;

end;

x3 in U_FT (y2,0) by A16, FINTOPO3:47;
then p in U_FT (q,0) by A8, A17;
then A20: p in U_FT q by FINTOPO3:47;
q in U_FT (x,k) by A8, A11, A15;
then p in (U_FT (x,k)) ^f by A20;
hence (h ") . w in U_FT (x,(k + 1)) by A8, A13, FINTOPO3:48; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A21: g . y = x by A2, A4, A3, A8, FUNCT_1:34;
for w being Element of FT2 st w in U_FT (y,0) holds
(h ") . w in U_FT (x,0)

proof

let w be Element of FT2; :: thesis: ( w in U_FT (y,0) implies (h ") . w in U_FT (x,0) )
w in the carrier of FT2 ;
then A22: w in dom g by FUNCT_2:def 1;
A23: g .: (U_FT y) = Class ( the InternalRel of FT1,(g . y)) by A9;

hereby :: thesis: verum

assume w in U_FT (y,0) ; :: thesis: (h ") . w in U_FT (x,0)
then w in U_FT y by FINTOPO3:47;
then g . w in U_FT x by A21, A23, A22, FUNCT_1:def 6;
hence (h ") . w in U_FT (x,0) by A8, FINTOPO3:47; :: thesis: verum

end;

end;

then A24: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A24, A10);
then (h ") . (h . z) in U_FT (x,n) by A7;
hence z in U_FT (x,n) by A3, A5, FUNCT_1:34; :: thesis: verum

end;

now :: thesis: ( z in U_FT (x,n) implies h . z in U_FT (y,n) )

defpred S₁[ Nat] means for w being Element of FT1 st w in U_FT (x,$1) holds
h . w in U_FT (y,$1);
assume A25: z in U_FT (x,n) ; :: thesis: h . z in U_FT (y,n)
A26: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A27: S₁[k] ; :: thesis: S₁[k + 1]
for w being Element of FT1 st w in U_FT (x,(k + 1)) holds
h . w in U_FT (y,(k + 1))

proof

let w be Element of FT1; :: thesis: ( w in U_FT (x,(k + 1)) implies h . w in U_FT (y,(k + 1)) )
A28: U_FT (x,(k + 1)) = (U_FT (x,k)) ^f by FINTOPO3:48;
assume w in U_FT (x,(k + 1)) ; :: thesis: h . w in U_FT (y,(k + 1))
then consider x3 being Element of FT1 such that
A29: x3 = w and
A30: ex y3 being Element of FT1 st
( y3 in U_FT (x,k) & x3 in U_FT y3 ) by A28;
consider y2 being Element of FT1 such that
A31: y2 in U_FT (x,k) and
A32: x3 in U_FT y2 by A30;
reconsider q = h . y2, p = h . x3 as Element of FT2 ;
A33: for w2 being Element of FT1 st w2 in U_FT (y2,0) holds
h . w2 in U_FT (q,0)

proof

let w2 be Element of FT1; :: thesis: ( w2 in U_FT (y2,0) implies h . w2 in U_FT (q,0) )
w2 in the carrier of FT1 ;
then A34: w2 in dom h by FUNCT_2:def 1;
A35: h .: (U_FT y2) = Class ( the InternalRel of FT2,(h . y2)) by A1;

hereby :: thesis: verum

assume w2 in U_FT (y2,0) ; :: thesis: h . w2 in U_FT (q,0)
then w2 in U_FT y2 by FINTOPO3:47;
then h . w2 in U_FT q by A35, A34, FUNCT_1:def 6;
hence h . w2 in U_FT (q,0) by FINTOPO3:47; :: thesis: verum

end;

end;

x3 in U_FT (y2,0) by A32, FINTOPO3:47;
then p in U_FT (q,0) by A33;
then A36: p in U_FT q by FINTOPO3:47;
q in U_FT (y,k) by A27, A31;
then p in (U_FT (y,k)) ^f by A36;
hence h . w in U_FT (y,(k + 1)) by A29, FINTOPO3:48; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for w being Element of FT1 st w in U_FT (x,0) holds
h . w in U_FT (y,0)

proof

let w be Element of FT1; :: thesis: ( w in U_FT (x,0) implies h . w in U_FT (y,0) )
w in the carrier of FT1 ;
then A37: w in dom h by FUNCT_2:def 1;
A38: h .: (U_FT x) = Class ( the InternalRel of FT2,(h . x)) by A1;

hereby :: thesis: verum

assume w in U_FT (x,0) ; :: thesis: h . w in U_FT (y,0)
then w in U_FT x by FINTOPO3:47;
then h . w in U_FT y by A2, A38, A37, FUNCT_1:def 6;
hence h . w in U_FT (y,0) by FINTOPO3:47; :: thesis: verum

end;

end;

then A39: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A39, A26);
hence h . z in U_FT (y,n) by A25; :: thesis: verum

end;

hence ( z in U_FT (x,n) iff h . z in U_FT (y,n) ) by A6; :: thesis: verum