let a, b be Point of I[01]; :: thesis: for N being a_neighborhood of a * b ex N1 being a_neighborhood of a ex N2 being a_neighborhood of b st

for x, y being Point of I[01] st x in N1 & y in N2 holds

x * y in N

let N be a_neighborhood of a * b; :: thesis: ex N1 being a_neighborhood of a ex N2 being a_neighborhood of b st

for x, y being Point of I[01] st x in N1 & y in N2 holds

x * y in N

set g = I[01]-TIMES ;

I[01]-TIMES . (a,b) = a * b by Th6;

then consider H being a_neighborhood of [a,b] such that

A1: I[01]-TIMES .: H c= N by BORSUK_1:def 1;

consider F being Subset-Family of [:I[01],I[01]:] such that

A2: Int H = union F and

A3: for e being set st e in F holds

ex X1, Y1 being Subset of I[01] st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;

[a,b] in Int H by CONNSP_2:def 1;

then consider M being set such that

A4: [a,b] in M and

A5: M in F by A2, TARSKI:def 4;

consider A, B being Subset of I[01] such that

A6: M = [:A,B:] and

A7: A is open and

A8: B is open by A3, A5;

a in A by A4, A6, ZFMISC_1:87;

then A9: a in Int A by A7, TOPS_1:23;

b in B by A4, A6, ZFMISC_1:87;

then b in Int B by A8, TOPS_1:23;

then reconsider B = B as open a_neighborhood of b by A8, CONNSP_2:def 1;

reconsider A = A as open a_neighborhood of a by A7, A9, CONNSP_2:def 1;

take A ; :: thesis: ex N2 being a_neighborhood of b st

for x, y being Point of I[01] st x in A & y in N2 holds

x * y in N

take B ; :: thesis: for x, y being Point of I[01] st x in A & y in B holds

x * y in N

let x, y be Point of I[01]; :: thesis: ( x in A & y in B implies x * y in N )

assume A10: ( x in A & y in B ) ; :: thesis: x * y in N

A11: Int H c= H by TOPS_1:16;

A12: I[01]-TIMES . (x,y) = x * y by Th6;

[x,y] in M by A6, A10, ZFMISC_1:87;

then [x,y] in Int H by A2, A5, TARSKI:def 4;

then I[01]-TIMES . (x,y) in I[01]-TIMES .: H by A11, FUNCT_2:35;

hence x * y in N by A1, A12; :: thesis: verum

for x, y being Point of I[01] st x in N1 & y in N2 holds

x * y in N

let N be a_neighborhood of a * b; :: thesis: ex N1 being a_neighborhood of a ex N2 being a_neighborhood of b st

for x, y being Point of I[01] st x in N1 & y in N2 holds

x * y in N

set g = I[01]-TIMES ;

I[01]-TIMES . (a,b) = a * b by Th6;

then consider H being a_neighborhood of [a,b] such that

A1: I[01]-TIMES .: H c= N by BORSUK_1:def 1;

consider F being Subset-Family of [:I[01],I[01]:] such that

A2: Int H = union F and

A3: for e being set st e in F holds

ex X1, Y1 being Subset of I[01] st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;

[a,b] in Int H by CONNSP_2:def 1;

then consider M being set such that

A4: [a,b] in M and

A5: M in F by A2, TARSKI:def 4;

consider A, B being Subset of I[01] such that

A6: M = [:A,B:] and

A7: A is open and

A8: B is open by A3, A5;

a in A by A4, A6, ZFMISC_1:87;

then A9: a in Int A by A7, TOPS_1:23;

b in B by A4, A6, ZFMISC_1:87;

then b in Int B by A8, TOPS_1:23;

then reconsider B = B as open a_neighborhood of b by A8, CONNSP_2:def 1;

reconsider A = A as open a_neighborhood of a by A7, A9, CONNSP_2:def 1;

take A ; :: thesis: ex N2 being a_neighborhood of b st

for x, y being Point of I[01] st x in A & y in N2 holds

x * y in N

take B ; :: thesis: for x, y being Point of I[01] st x in A & y in B holds

x * y in N

let x, y be Point of I[01]; :: thesis: ( x in A & y in B implies x * y in N )

assume A10: ( x in A & y in B ) ; :: thesis: x * y in N

A11: Int H c= H by TOPS_1:16;

A12: I[01]-TIMES . (x,y) = x * y by Th6;

[x,y] in M by A6, A10, ZFMISC_1:87;

then [x,y] in Int H by A2, A5, TARSKI:def 4;

then I[01]-TIMES . (x,y) in I[01]-TIMES .: H by A11, FUNCT_2:35;

hence x * y in N by A1, A12; :: thesis: verum