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 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 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 z being Element of FT1 holds
( z in U_FT x,n iff h . z 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 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, Def1;
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

defpred S₁[ Element of 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 Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of 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, Def1;

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 12;
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:56;
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, Def1;

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 12;
hence (h " ) . w in U_FT x,0 by A8, FINTOPO3:47; :: thesis: verum

end;

end;

then A24: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(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:56; :: thesis: verum

end;

now

defpred S₁[ Element of 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 Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of 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, Def1;

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 12;
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, Def1;

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 12;
hence h . w in U_FT y,0 by FINTOPO3:47; :: thesis: verum

end;

end;

then A39: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(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