let n, m be Nat; :: thesis: for T being non empty TopSpace

for A, B being Subset of T

for r, s being Real st r > 0 & s > 0 holds

for pA being Point of (TOP-REAL n)

for pB being Point of (TOP-REAL m) st T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m

let T be non empty TopSpace; :: thesis: for A, B being Subset of T

for r, s being Real st r > 0 & s > 0 holds

for pA being Point of (TOP-REAL n)

for pB being Point of (TOP-REAL m) st T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m

let A, B be Subset of T; :: thesis: for r, s being Real st r > 0 & s > 0 holds

for pA being Point of (TOP-REAL n)

for pB being Point of (TOP-REAL m) st T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m

let r, s be Real; :: thesis: ( r > 0 & s > 0 implies for pA being Point of (TOP-REAL n)

for pB being Point of (TOP-REAL m) st T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m )

assume that

A1: r > 0 and

A2: s > 0 ; :: thesis: for pA being Point of (TOP-REAL n)

for pB being Point of (TOP-REAL m) st T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m

let pA be Point of (TOP-REAL n); :: thesis: for pB being Point of (TOP-REAL m) st T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m

let pB be Point of (TOP-REAL m); :: thesis: ( T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B implies n = m )

assume that

A3: T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic and

A4: T | B, Tdisk (pB,s) are_homeomorphic and

A5: Int A meets Int B ; :: thesis: n = m

A6: Int A c= A by TOPS_1:16;

set TBALL = (TOP-REAL n) | (Ball (pA,r));

consider hA being Function of (T | A),((TOP-REAL n) | (Ball (pA,r))) such that

A7: hA is being_homeomorphism by A3, T_0TOPSP:def 1;

A8: (Int A) /\ (Int B) c= Int A by XBOOLE_1:17;

A9: [#] (T | A) = A by PRE_TOPC:def 5;

then reconsider IA = (Int A) /\ (Int B) as Subset of (T | A) by A6, A8, XBOOLE_1:1;

A10: (T | A) | IA = T | ((Int A) /\ (Int B)) by A6, A8, XBOOLE_1:1, PRE_TOPC:7;

A11: [#] ((TOP-REAL n) | (Ball (pA,r))) = Ball (pA,r) by PRE_TOPC:def 5;

then reconsider hAI = hA .: IA as Subset of (TOP-REAL n) by XBOOLE_1:1;

A12: (Int A) /\ (Int B) in the topology of T by PRE_TOPC:def 2;

not (Int A) /\ (Int B) is empty by A5;

then consider p being set such that

A13: p in (Int A) /\ (Int B) ;

reconsider p = p as Point of T by A13;

A14: dom hA = [#] (T | A) by A7, TOPS_2:def 5;

then A15: hA . p in hA .: IA by A13, FUNCT_1:def 6;

p in Int A by A13, XBOOLE_0:def 4;

then not (TOP-REAL n) | (Ball (pA,r)) is empty by A14, A6;

then reconsider g = hA | IA as Function of ((T | A) | IA),(((TOP-REAL n) | (Ball (pA,r))) | (hA .: IA)) by A13, JORDAN24:12;

A16: Int B c= B by TOPS_1:16;

IA /\ A = IA by A6, A8, XBOOLE_1:1, XBOOLE_1:28;

then IA in the topology of (T | A) by A12, A9, PRE_TOPC:def 4;

then IA is open by PRE_TOPC:def 2;

then hA .: IA is open by A13, A7, TOPGRP_1:25, A1;

then hAI is open by A11, TSEP_1:9;

then not Int hAI is empty by TOPS_1:23, A15;

then A17: not hAI is boundary ;

consider hB being Function of (T | B),(Tdisk (pB,s)) such that

A18: hB is being_homeomorphism by A4, T_0TOPSP:def 1;

A19: ((TOP-REAL n) | (Ball (pA,r))) | (hA .: IA) = (TOP-REAL n) | hAI by PRE_TOPC:7, A11;

then reconsider G = g as Function of (T | ((Int A) /\ (Int B))),((TOP-REAL n) | hAI) by A10;

A20: (Int A) /\ (Int B) c= Int B by XBOOLE_1:17;

A21: [#] (T | B) = B by PRE_TOPC:def 5;

then reconsider IB = (Int A) /\ (Int B) as Subset of (T | B) by A16, A20, XBOOLE_1:1;

A22: (T | B) | IB = T | ((Int A) /\ (Int B)) by A16, A20, XBOOLE_1:1, PRE_TOPC:7;

A23: dom hB = [#] (T | B) by A18, TOPS_2:def 5;

then A24: hB . p in hB .: IB by A13, FUNCT_1:def 6;

p in Int B by A13, XBOOLE_0:def 4;

then not Tdisk (pB,s) is empty by A23, A16;

then reconsider f = hB | IB as Function of ((T | B) | IB),((Tdisk (pB,s)) | (hB .: IB)) by A13, JORDAN24:12;

A25: [#] (Tdisk (pB,s)) = cl_Ball (pB,s) by PRE_TOPC:def 5;

then reconsider hBI = hB .: IB as Subset of (TOP-REAL m) by XBOOLE_1:1;

A26: (Tdisk (pB,s)) | (hB .: IB) = (TOP-REAL m) | hBI by PRE_TOPC:7, A25;

then reconsider F = f as Function of (T | ((Int A) /\ (Int B))),((TOP-REAL m) | hBI) by A22;

F is being_homeomorphism by A18, METRIZTS:2, A26, A22;

then A27: F " is being_homeomorphism by TOPS_2:56, A24;

reconsider GF = G * (F ") as Function of ((TOP-REAL m) | hBI),((TOP-REAL n) | hAI) by A13;

G is being_homeomorphism by A7, METRIZTS:2, A19, A10;

then GF is being_homeomorphism by A27, TOPS_2:57, A15, A24, A13;

then hBI,hAI are_homeomorphic by T_0TOPSP:def 1, METRIZTS:def 1;

then A28: ind hBI = ind hAI by TOPDIM_1:27;

IB /\ B = IB by A16, A20, XBOOLE_1:1, XBOOLE_1:28;

then IB in the topology of (T | B) by A12, A21, PRE_TOPC:def 4;

then IB is open by PRE_TOPC:def 2;

then hB .: IB is open by A13, A18, TOPGRP_1:25, A2;

then not Int hBI is empty by A13, A2, Th13;

then not hBI is boundary ;

then ind hBI = m by Th6;

hence n = m by A17, Th6, A28; :: thesis: verum

for A, B being Subset of T

for r, s being Real st r > 0 & s > 0 holds

for pA being Point of (TOP-REAL n)

for pB being Point of (TOP-REAL m) st T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m

let T be non empty TopSpace; :: thesis: for A, B being Subset of T

for r, s being Real st r > 0 & s > 0 holds

for pA being Point of (TOP-REAL n)

for pB being Point of (TOP-REAL m) st T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m

let A, B be Subset of T; :: thesis: for r, s being Real st r > 0 & s > 0 holds

for pA being Point of (TOP-REAL n)

for pB being Point of (TOP-REAL m) st T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m

let r, s be Real; :: thesis: ( r > 0 & s > 0 implies for pA being Point of (TOP-REAL n)

for pB being Point of (TOP-REAL m) st T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m )

assume that

A1: r > 0 and

A2: s > 0 ; :: thesis: for pA being Point of (TOP-REAL n)

for pB being Point of (TOP-REAL m) st T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m

let pA be Point of (TOP-REAL n); :: thesis: for pB being Point of (TOP-REAL m) st T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m

let pB be Point of (TOP-REAL m); :: thesis: ( T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B implies n = m )

assume that

A3: T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic and

A4: T | B, Tdisk (pB,s) are_homeomorphic and

A5: Int A meets Int B ; :: thesis: n = m

A6: Int A c= A by TOPS_1:16;

set TBALL = (TOP-REAL n) | (Ball (pA,r));

consider hA being Function of (T | A),((TOP-REAL n) | (Ball (pA,r))) such that

A7: hA is being_homeomorphism by A3, T_0TOPSP:def 1;

A8: (Int A) /\ (Int B) c= Int A by XBOOLE_1:17;

A9: [#] (T | A) = A by PRE_TOPC:def 5;

then reconsider IA = (Int A) /\ (Int B) as Subset of (T | A) by A6, A8, XBOOLE_1:1;

A10: (T | A) | IA = T | ((Int A) /\ (Int B)) by A6, A8, XBOOLE_1:1, PRE_TOPC:7;

A11: [#] ((TOP-REAL n) | (Ball (pA,r))) = Ball (pA,r) by PRE_TOPC:def 5;

then reconsider hAI = hA .: IA as Subset of (TOP-REAL n) by XBOOLE_1:1;

A12: (Int A) /\ (Int B) in the topology of T by PRE_TOPC:def 2;

not (Int A) /\ (Int B) is empty by A5;

then consider p being set such that

A13: p in (Int A) /\ (Int B) ;

reconsider p = p as Point of T by A13;

A14: dom hA = [#] (T | A) by A7, TOPS_2:def 5;

then A15: hA . p in hA .: IA by A13, FUNCT_1:def 6;

p in Int A by A13, XBOOLE_0:def 4;

then not (TOP-REAL n) | (Ball (pA,r)) is empty by A14, A6;

then reconsider g = hA | IA as Function of ((T | A) | IA),(((TOP-REAL n) | (Ball (pA,r))) | (hA .: IA)) by A13, JORDAN24:12;

A16: Int B c= B by TOPS_1:16;

IA /\ A = IA by A6, A8, XBOOLE_1:1, XBOOLE_1:28;

then IA in the topology of (T | A) by A12, A9, PRE_TOPC:def 4;

then IA is open by PRE_TOPC:def 2;

then hA .: IA is open by A13, A7, TOPGRP_1:25, A1;

then hAI is open by A11, TSEP_1:9;

then not Int hAI is empty by TOPS_1:23, A15;

then A17: not hAI is boundary ;

consider hB being Function of (T | B),(Tdisk (pB,s)) such that

A18: hB is being_homeomorphism by A4, T_0TOPSP:def 1;

A19: ((TOP-REAL n) | (Ball (pA,r))) | (hA .: IA) = (TOP-REAL n) | hAI by PRE_TOPC:7, A11;

then reconsider G = g as Function of (T | ((Int A) /\ (Int B))),((TOP-REAL n) | hAI) by A10;

A20: (Int A) /\ (Int B) c= Int B by XBOOLE_1:17;

A21: [#] (T | B) = B by PRE_TOPC:def 5;

then reconsider IB = (Int A) /\ (Int B) as Subset of (T | B) by A16, A20, XBOOLE_1:1;

A22: (T | B) | IB = T | ((Int A) /\ (Int B)) by A16, A20, XBOOLE_1:1, PRE_TOPC:7;

A23: dom hB = [#] (T | B) by A18, TOPS_2:def 5;

then A24: hB . p in hB .: IB by A13, FUNCT_1:def 6;

p in Int B by A13, XBOOLE_0:def 4;

then not Tdisk (pB,s) is empty by A23, A16;

then reconsider f = hB | IB as Function of ((T | B) | IB),((Tdisk (pB,s)) | (hB .: IB)) by A13, JORDAN24:12;

A25: [#] (Tdisk (pB,s)) = cl_Ball (pB,s) by PRE_TOPC:def 5;

then reconsider hBI = hB .: IB as Subset of (TOP-REAL m) by XBOOLE_1:1;

A26: (Tdisk (pB,s)) | (hB .: IB) = (TOP-REAL m) | hBI by PRE_TOPC:7, A25;

then reconsider F = f as Function of (T | ((Int A) /\ (Int B))),((TOP-REAL m) | hBI) by A22;

F is being_homeomorphism by A18, METRIZTS:2, A26, A22;

then A27: F " is being_homeomorphism by TOPS_2:56, A24;

reconsider GF = G * (F ") as Function of ((TOP-REAL m) | hBI),((TOP-REAL n) | hAI) by A13;

G is being_homeomorphism by A7, METRIZTS:2, A19, A10;

then GF is being_homeomorphism by A27, TOPS_2:57, A15, A24, A13;

then hBI,hAI are_homeomorphic by T_0TOPSP:def 1, METRIZTS:def 1;

then A28: ind hBI = ind hAI by TOPDIM_1:27;

IB /\ B = IB by A16, A20, XBOOLE_1:1, XBOOLE_1:28;

then IB in the topology of (T | B) by A12, A21, PRE_TOPC:def 4;

then IB is open by PRE_TOPC:def 2;

then hB .: IB is open by A13, A18, TOPGRP_1:25, A2;

then not Int hBI is empty by A13, A2, Th13;

then not hBI is boundary ;

then ind hBI = m by Th6;

hence n = m by A17, Th6, A28; :: thesis: verum