let N, M be non empty locally_euclidean TopSpace; :: thesis: Int [:N,M:] = [:(Int N),(Int M):]

set NM = [:N,M:];

set IN = Int N;

set IM = Int M;

thus Int [:N,M:] c= [:(Int N),(Int M):] :: according to XBOOLE_0:def 10 :: thesis: [:(Int N),(Int M):] c= Int [:N,M:]

assume A53: z in [:(Int N),(Int M):] ; :: thesis: z in Int [:N,M:]

then consider x, y being object such that

A54: x in Int N and

A55: y in Int M and

A56: z = [x,y] by ZFMISC_1:def 2;

reconsider x = x as Point of N by A54;

consider U being a_neighborhood of x, n being Nat such that

A57: N | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A54, Def4;

reconsider y = y as Point of M by A55;

consider W being a_neighborhood of y, m being Nat such that

A58: M | W, Tball ((0. (TOP-REAL m)),1) are_homeomorphic by A55, Def4;

reconsider p = z as Point of [:N,M:] by A53;

set TRn = TOP-REAL n;

set TRm = TOP-REAL m;

reconsider mn = m + n as Nat ;

[:(N | U),(M | W):],(TOP-REAL mn) | (Ball ((0. (TOP-REAL mn)),1)) are_homeomorphic by A57, A58, TIETZE_2:20;

then [:N,M:] | [:U,W:], Tball ((0. (TOP-REAL mn)),1) are_homeomorphic by BORSUK_3:22;

hence z in Int [:N,M:] by Def4, A56; :: thesis: verum

set NM = [:N,M:];

set IN = Int N;

set IM = Int M;

thus Int [:N,M:] c= [:(Int N),(Int M):] :: according to XBOOLE_0:def 10 :: thesis: [:(Int N),(Int M):] c= Int [:N,M:]

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [:(Int N),(Int M):] or z in Int [:N,M:] )
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Int [:N,M:] or z in [:(Int N),(Int M):] )

assume A1: z in Int [:N,M:] ; :: thesis: z in [:(Int N),(Int M):]

then reconsider p = z as Point of [:N,M:] ;

z in the carrier of [:N,M:] by A1;

then z in [: the carrier of N, the carrier of M:] by BORSUK_1:def 2;

then consider x, y being object such that

A2: x in the carrier of N and

A3: y in the carrier of M and

A4: z = [x,y] by ZFMISC_1:def 2;

reconsider y = y as Point of M by A3;

reconsider x = x as Point of N by A2;

assume A5: not z in [:(Int N),(Int M):] ; :: thesis: contradiction

end;assume A1: z in Int [:N,M:] ; :: thesis: z in [:(Int N),(Int M):]

then reconsider p = z as Point of [:N,M:] ;

z in the carrier of [:N,M:] by A1;

then z in [: the carrier of N, the carrier of M:] by BORSUK_1:def 2;

then consider x, y being object such that

A2: x in the carrier of N and

A3: y in the carrier of M and

A4: z = [x,y] by ZFMISC_1:def 2;

reconsider y = y as Point of M by A3;

reconsider x = x as Point of N by A2;

assume A5: not z in [:(Int N),(Int M):] ; :: thesis: contradiction

per cases
( not x in Int N or not y in Int M )
by A5, A4, ZFMISC_1:87;

end;

suppose A6:
not x in Int N
; :: thesis: contradiction

consider W being a_neighborhood of y, m being Nat such that

A7: M | W, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic by Def2;

x in ([#] N) \ (Int N) by A6, XBOOLE_0:def 5;

then x in Fr N by SUBSET_1:def 4;

then consider U being a_neighborhood of x, n being Nat, h being Function of (N | U),(Tdisk ((0. (TOP-REAL n)),1)) such that

A8: h is being_homeomorphism and

A9: h . x in Sphere ((0. (TOP-REAL n)),1) by Th5;

A10: y in Int W by CONNSP_2:def 1;

reconsider mn = m + n as Nat ;

set TRm = TOP-REAL m;

set TRn = TOP-REAL n;

set TRnm = TOP-REAL mn;

consider f being Function of (M | W),(Tdisk ((0. (TOP-REAL m)),1)) such that

A11: f is being_homeomorphism by A7, T_0TOPSP:def 1;

A12: not h . x in Ball ((0. (TOP-REAL n)),1) by TOPREAL9:19, A9, XBOOLE_0:3;

consider hf being Function of [:(Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL m)),1)):],(Tdisk ((0. (TOP-REAL mn)),1)) such that

A13: hf is being_homeomorphism and

A14: hf .: [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] = Ball ((0. (TOP-REAL mn)),1) by TIETZE_2:19;

set H = hf * [:h,f:];

[:h,f:] is being_homeomorphism by A8, A11, TIETZE_2:15;

then A15: hf * [:h,f:] is being_homeomorphism by A13, TOPS_2:57;

then A16: rng (hf * [:h,f:]) = [#] (Tdisk ((0. (TOP-REAL mn)),1)) by TOPS_2:def 5;

A17: Int W c= W by TOPS_1:16;

A18: Int U c= U by TOPS_1:16;

x in Int U by CONNSP_2:def 1;

then A19: [x,y] in [:U,W:] by A18, A17, A10, ZFMISC_1:87;

n + m in NAT by ORDINAL1:def 12;

then A20: [#] (Tdisk ((0. (TOP-REAL mn)),1)) = cl_Ball ((0. (TOP-REAL mn)),1) by BROUWER:3;

A21: [:(N | U),(M | W):] = [:N,M:] | [:U,W:] by BORSUK_3:22;

then dom (hf * [:h,f:]) = [#] ([:N,M:] | [:U,W:]) by A15, TOPS_2:def 5;

then A22: p in dom (hf * [:h,f:]) by A19, A4, PRE_TOPC:def 5;

then A23: [:h,f:] . p in dom hf by FUNCT_1:11;

dom [:h,f:] = [:(dom h),(dom f):] by FUNCT_3:def 8;

then A24: [:h,f:] . (x,y) = [(h . x),(f . y)] by A22, FUNCT_1:11, A4, FUNCT_3:65;

A25: (hf * [:h,f:]) . p = hf . ([:h,f:] . p) by A22, FUNCT_1:12;

(hf * [:h,f:]) . p in Sphere ((0. (TOP-REAL mn)),1)

then p in ([#] [:N,M:]) \ (Int [:N,M:]) by SUBSET_1:def 4;

hence contradiction by XBOOLE_0:def 5, A1; :: thesis: verum

end;A7: M | W, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic by Def2;

x in ([#] N) \ (Int N) by A6, XBOOLE_0:def 5;

then x in Fr N by SUBSET_1:def 4;

then consider U being a_neighborhood of x, n being Nat, h being Function of (N | U),(Tdisk ((0. (TOP-REAL n)),1)) such that

A8: h is being_homeomorphism and

A9: h . x in Sphere ((0. (TOP-REAL n)),1) by Th5;

A10: y in Int W by CONNSP_2:def 1;

reconsider mn = m + n as Nat ;

set TRm = TOP-REAL m;

set TRn = TOP-REAL n;

set TRnm = TOP-REAL mn;

consider f being Function of (M | W),(Tdisk ((0. (TOP-REAL m)),1)) such that

A11: f is being_homeomorphism by A7, T_0TOPSP:def 1;

A12: not h . x in Ball ((0. (TOP-REAL n)),1) by TOPREAL9:19, A9, XBOOLE_0:3;

consider hf being Function of [:(Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL m)),1)):],(Tdisk ((0. (TOP-REAL mn)),1)) such that

A13: hf is being_homeomorphism and

A14: hf .: [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] = Ball ((0. (TOP-REAL mn)),1) by TIETZE_2:19;

set H = hf * [:h,f:];

[:h,f:] is being_homeomorphism by A8, A11, TIETZE_2:15;

then A15: hf * [:h,f:] is being_homeomorphism by A13, TOPS_2:57;

then A16: rng (hf * [:h,f:]) = [#] (Tdisk ((0. (TOP-REAL mn)),1)) by TOPS_2:def 5;

A17: Int W c= W by TOPS_1:16;

A18: Int U c= U by TOPS_1:16;

x in Int U by CONNSP_2:def 1;

then A19: [x,y] in [:U,W:] by A18, A17, A10, ZFMISC_1:87;

n + m in NAT by ORDINAL1:def 12;

then A20: [#] (Tdisk ((0. (TOP-REAL mn)),1)) = cl_Ball ((0. (TOP-REAL mn)),1) by BROUWER:3;

A21: [:(N | U),(M | W):] = [:N,M:] | [:U,W:] by BORSUK_3:22;

then dom (hf * [:h,f:]) = [#] ([:N,M:] | [:U,W:]) by A15, TOPS_2:def 5;

then A22: p in dom (hf * [:h,f:]) by A19, A4, PRE_TOPC:def 5;

then A23: [:h,f:] . p in dom hf by FUNCT_1:11;

dom [:h,f:] = [:(dom h),(dom f):] by FUNCT_3:def 8;

then A24: [:h,f:] . (x,y) = [(h . x),(f . y)] by A22, FUNCT_1:11, A4, FUNCT_3:65;

A25: (hf * [:h,f:]) . p = hf . ([:h,f:] . p) by A22, FUNCT_1:12;

(hf * [:h,f:]) . p in Sphere ((0. (TOP-REAL mn)),1)

proof

then
p in Fr [:N,M:]
by A21, A4, Th5, A15;
(hf * [:h,f:]) . p in cl_Ball ((0. (TOP-REAL mn)),1)
by A16, A20, A22, FUNCT_1:def 3;

then A26: (hf * [:h,f:]) . p in (Sphere ((0. (TOP-REAL mn)),1)) \/ (Ball ((0. (TOP-REAL mn)),1)) by TOPREAL9:18;

assume not (hf * [:h,f:]) . p in Sphere ((0. (TOP-REAL mn)),1) ; :: thesis: contradiction

then (hf * [:h,f:]) . p in hf .: [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] by A26, XBOOLE_0:def 3, A14;

then consider w being object such that

A27: w in dom hf and

A28: w in [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] and

A29: hf . w = (hf * [:h,f:]) . p by FUNCT_1:def 6;

w = [:h,f:] . p by A25, A23, A13, A27, A29, FUNCT_1:def 4;

hence contradiction by A28, A4, A24, A12, ZFMISC_1:87; :: thesis: verum

end;then A26: (hf * [:h,f:]) . p in (Sphere ((0. (TOP-REAL mn)),1)) \/ (Ball ((0. (TOP-REAL mn)),1)) by TOPREAL9:18;

assume not (hf * [:h,f:]) . p in Sphere ((0. (TOP-REAL mn)),1) ; :: thesis: contradiction

then (hf * [:h,f:]) . p in hf .: [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] by A26, XBOOLE_0:def 3, A14;

then consider w being object such that

A27: w in dom hf and

A28: w in [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] and

A29: hf . w = (hf * [:h,f:]) . p by FUNCT_1:def 6;

w = [:h,f:] . p by A25, A23, A13, A27, A29, FUNCT_1:def 4;

hence contradiction by A28, A4, A24, A12, ZFMISC_1:87; :: thesis: verum

then p in ([#] [:N,M:]) \ (Int [:N,M:]) by SUBSET_1:def 4;

hence contradiction by XBOOLE_0:def 5, A1; :: thesis: verum

suppose
not y in Int M
; :: thesis: contradiction

then
y in ([#] M) \ (Int M)
by XBOOLE_0:def 5;

then y in Fr M by SUBSET_1:def 4;

then consider W being a_neighborhood of y, m being Nat, f being Function of (M | W),(Tdisk ((0. (TOP-REAL m)),1)) such that

A30: f is being_homeomorphism and

A31: f . y in Sphere ((0. (TOP-REAL m)),1) by Th5;

A32: y in Int W by CONNSP_2:def 1;

consider U being a_neighborhood of x, n being Nat such that

A33: N | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def2;

reconsider mn = n + m as Nat ;

set TRm = TOP-REAL m;

set TRn = TOP-REAL n;

set TRnm = TOP-REAL mn;

consider h being Function of (N | U),(Tdisk ((0. (TOP-REAL n)),1)) such that

A34: h is being_homeomorphism by A33, T_0TOPSP:def 1;

A35: not f . y in Ball ((0. (TOP-REAL m)),1) by TOPREAL9:19, A31, XBOOLE_0:3;

consider hf being Function of [:(Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL m)),1)):],(Tdisk ((0. (TOP-REAL mn)),1)) such that

A36: hf is being_homeomorphism and

A37: hf .: [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] = Ball ((0. (TOP-REAL mn)),1) by TIETZE_2:19;

set H = hf * [:h,f:];

[:h,f:] is being_homeomorphism by A30, A34, TIETZE_2:15;

then A38: hf * [:h,f:] is being_homeomorphism by A36, TOPS_2:57;

then A39: rng (hf * [:h,f:]) = [#] (Tdisk ((0. (TOP-REAL mn)),1)) by TOPS_2:def 5;

A40: Int W c= W by TOPS_1:16;

A41: Int U c= U by TOPS_1:16;

x in Int U by CONNSP_2:def 1;

then A42: [x,y] in [:U,W:] by A41, A40, A32, ZFMISC_1:87;

n + m in NAT by ORDINAL1:def 12;

then A43: [#] (Tdisk ((0. (TOP-REAL mn)),1)) = cl_Ball ((0. (TOP-REAL mn)),1) by BROUWER:3;

A44: [:(N | U),(M | W):] = [:N,M:] | [:U,W:] by BORSUK_3:22;

then dom (hf * [:h,f:]) = [#] ([:N,M:] | [:U,W:]) by A38, TOPS_2:def 5;

then A45: p in dom (hf * [:h,f:]) by A42, A4, PRE_TOPC:def 5;

then A46: [:h,f:] . p in dom hf by FUNCT_1:11;

dom [:h,f:] = [:(dom h),(dom f):] by FUNCT_3:def 8;

then A47: [:h,f:] . (x,y) = [(h . x),(f . y)] by A45, FUNCT_1:11, A4, FUNCT_3:65;

A48: (hf * [:h,f:]) . p = hf . ([:h,f:] . p) by A45, FUNCT_1:12;

(hf * [:h,f:]) . p in Sphere ((0. (TOP-REAL mn)),1)

then p in ([#] [:N,M:]) \ (Int [:N,M:]) by SUBSET_1:def 4;

hence contradiction by XBOOLE_0:def 5, A1; :: thesis: verum

end;then y in Fr M by SUBSET_1:def 4;

then consider W being a_neighborhood of y, m being Nat, f being Function of (M | W),(Tdisk ((0. (TOP-REAL m)),1)) such that

A30: f is being_homeomorphism and

A31: f . y in Sphere ((0. (TOP-REAL m)),1) by Th5;

A32: y in Int W by CONNSP_2:def 1;

consider U being a_neighborhood of x, n being Nat such that

A33: N | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def2;

reconsider mn = n + m as Nat ;

set TRm = TOP-REAL m;

set TRn = TOP-REAL n;

set TRnm = TOP-REAL mn;

consider h being Function of (N | U),(Tdisk ((0. (TOP-REAL n)),1)) such that

A34: h is being_homeomorphism by A33, T_0TOPSP:def 1;

A35: not f . y in Ball ((0. (TOP-REAL m)),1) by TOPREAL9:19, A31, XBOOLE_0:3;

consider hf being Function of [:(Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL m)),1)):],(Tdisk ((0. (TOP-REAL mn)),1)) such that

A36: hf is being_homeomorphism and

A37: hf .: [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] = Ball ((0. (TOP-REAL mn)),1) by TIETZE_2:19;

set H = hf * [:h,f:];

[:h,f:] is being_homeomorphism by A30, A34, TIETZE_2:15;

then A38: hf * [:h,f:] is being_homeomorphism by A36, TOPS_2:57;

then A39: rng (hf * [:h,f:]) = [#] (Tdisk ((0. (TOP-REAL mn)),1)) by TOPS_2:def 5;

A40: Int W c= W by TOPS_1:16;

A41: Int U c= U by TOPS_1:16;

x in Int U by CONNSP_2:def 1;

then A42: [x,y] in [:U,W:] by A41, A40, A32, ZFMISC_1:87;

n + m in NAT by ORDINAL1:def 12;

then A43: [#] (Tdisk ((0. (TOP-REAL mn)),1)) = cl_Ball ((0. (TOP-REAL mn)),1) by BROUWER:3;

A44: [:(N | U),(M | W):] = [:N,M:] | [:U,W:] by BORSUK_3:22;

then dom (hf * [:h,f:]) = [#] ([:N,M:] | [:U,W:]) by A38, TOPS_2:def 5;

then A45: p in dom (hf * [:h,f:]) by A42, A4, PRE_TOPC:def 5;

then A46: [:h,f:] . p in dom hf by FUNCT_1:11;

dom [:h,f:] = [:(dom h),(dom f):] by FUNCT_3:def 8;

then A47: [:h,f:] . (x,y) = [(h . x),(f . y)] by A45, FUNCT_1:11, A4, FUNCT_3:65;

A48: (hf * [:h,f:]) . p = hf . ([:h,f:] . p) by A45, FUNCT_1:12;

(hf * [:h,f:]) . p in Sphere ((0. (TOP-REAL mn)),1)

proof

then
p in Fr [:N,M:]
by A44, A4, Th5, A38;
(hf * [:h,f:]) . p in cl_Ball ((0. (TOP-REAL mn)),1)
by A39, A43, A45, FUNCT_1:def 3;

then A49: (hf * [:h,f:]) . p in (Sphere ((0. (TOP-REAL mn)),1)) \/ (Ball ((0. (TOP-REAL mn)),1)) by TOPREAL9:18;

assume not (hf * [:h,f:]) . p in Sphere ((0. (TOP-REAL mn)),1) ; :: thesis: contradiction

then (hf * [:h,f:]) . p in hf .: [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] by A49, XBOOLE_0:def 3, A37;

then consider w being object such that

A50: w in dom hf and

A51: w in [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] and

A52: hf . w = (hf * [:h,f:]) . p by FUNCT_1:def 6;

w = [:h,f:] . p by A48, A46, A36, A50, A52, FUNCT_1:def 4;

hence contradiction by A51, A4, A47, A35, ZFMISC_1:87; :: thesis: verum

end;then A49: (hf * [:h,f:]) . p in (Sphere ((0. (TOP-REAL mn)),1)) \/ (Ball ((0. (TOP-REAL mn)),1)) by TOPREAL9:18;

assume not (hf * [:h,f:]) . p in Sphere ((0. (TOP-REAL mn)),1) ; :: thesis: contradiction

then (hf * [:h,f:]) . p in hf .: [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] by A49, XBOOLE_0:def 3, A37;

then consider w being object such that

A50: w in dom hf and

A51: w in [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] and

A52: hf . w = (hf * [:h,f:]) . p by FUNCT_1:def 6;

w = [:h,f:] . p by A48, A46, A36, A50, A52, FUNCT_1:def 4;

hence contradiction by A51, A4, A47, A35, ZFMISC_1:87; :: thesis: verum

then p in ([#] [:N,M:]) \ (Int [:N,M:]) by SUBSET_1:def 4;

hence contradiction by XBOOLE_0:def 5, A1; :: thesis: verum

assume A53: z in [:(Int N),(Int M):] ; :: thesis: z in Int [:N,M:]

then consider x, y being object such that

A54: x in Int N and

A55: y in Int M and

A56: z = [x,y] by ZFMISC_1:def 2;

reconsider x = x as Point of N by A54;

consider U being a_neighborhood of x, n being Nat such that

A57: N | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A54, Def4;

reconsider y = y as Point of M by A55;

consider W being a_neighborhood of y, m being Nat such that

A58: M | W, Tball ((0. (TOP-REAL m)),1) are_homeomorphic by A55, Def4;

reconsider p = z as Point of [:N,M:] by A53;

set TRn = TOP-REAL n;

set TRm = TOP-REAL m;

reconsider mn = m + n as Nat ;

[:(N | U),(M | W):],(TOP-REAL mn) | (Ball ((0. (TOP-REAL mn)),1)) are_homeomorphic by A57, A58, TIETZE_2:20;

then [:N,M:] | [:U,W:], Tball ((0. (TOP-REAL mn)),1) are_homeomorphic by BORSUK_3:22;

hence z in Int [:N,M:] by Def4, A56; :: thesis: verum