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;

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_{1}[ 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_{1}[k] holds

S_{1}[k + 1]

for w being Element of FT2 st w in U_FT (y,0) holds

(h ") . w in U_FT (x,0)_{1}[ 0 ]
;

for k being Nat holds S_{1}[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;(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

S

proof

A21:
g . y = x
by A2, A4, A3, A8, FUNCT_1:34;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A11: S_{1}[k]
; :: thesis: S_{1}[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))_{1}[k + 1]
; :: thesis: verum

end;assume A11: S

for w being Element of FT2 st w in U_FT (y,(k + 1)) holds

(h ") . w in U_FT (x,(k + 1))

proof

hence
S
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)

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;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

x3 in U_FT (y2,0)
by A16, FINTOPO3:47;
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;

end;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;

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

for w being Element of FT2 st w in U_FT (y,0) holds

(h ") . w in U_FT (x,0)

proof

then A24:
S
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;

end;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;

for k being Nat holds S

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

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

hence
( z in U_FT (x,n) iff h . z in U_FT (y,n) )
by A6; :: thesis: verumdefpred S_{1}[ 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_{1}[k] holds

S_{1}[k + 1]

h . w in U_FT (y,0)_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A39, A26);

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

end;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

S

proof

for w being Element of FT1 st w in U_FT (x,0) holds
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A27: S_{1}[k]
; :: thesis: S_{1}[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))_{1}[k + 1]
; :: thesis: verum

end;assume A27: S

for w being Element of FT1 st w in U_FT (x,(k + 1)) holds

h . w in U_FT (y,(k + 1))

proof

hence
S
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)

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;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

x3 in U_FT (y2,0)
by A32, FINTOPO3:47;
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;

end;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;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

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

h . w in U_FT (y,0)

proof

then A39:
S
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;

end;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;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

for k being Nat holds S

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