:: BORSUK_6 semantic presentation

REAL is non empty V32() complex-membered ext-real-membered real-membered V209() set

NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool REAL

bool REAL is non empty set

I[01] is non empty strict TopSpace-like T_0 T_1 T_2 V74() compact real-membered pathwise_connected SubSpace of R^1

R^1 is non empty strict TopSpace-like real-membered TopStruct

the carrier of I[01] is non empty complex-membered ext-real-membered real-membered set

omega is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() set

bool omega is non empty set

bool NAT is non empty set

{} is empty trivial Relation-like non-empty empty-yielding complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() set

the empty trivial Relation-like non-empty empty-yielding complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() set is empty trivial Relation-like non-empty empty-yielding complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() set

1 is non empty natural V11() real ext-real positive non negative V172() V173() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

{{},1} is non empty set

COMPLEX is non empty V32() complex-membered V209() set

RAT is non empty V32() complex-membered ext-real-membered real-membered rational-membered V209() set

INT is non empty V32() complex-membered ext-real-membered real-membered rational-membered integer-membered V209() set

[:REAL,REAL:] is non empty Relation-like set

bool [:REAL,REAL:] is non empty set

K457() is non empty V100() L9()

the carrier of K457() is non empty set

K462() is non empty V100() V174() V175() V176() V178() V225() V226() V227() V228() V229() V230() L9()

K463() is non empty V100() V176() V178() V228() V229() V230() M32(K462())

K464() is non empty V100() V174() V176() V178() V228() V229() V230() V231() M35(K462(),K463())

K466() is non empty V100() V174() V176() V178() L9()

K467() is non empty V100() V174() V176() V178() V231() M32(K466())

I[01] is non empty strict TopSpace-like T_0 T_1 T_2 V74() compact real-membered pathwise_connected TopStruct

the carrier of I[01] is non empty complex-membered ext-real-membered real-membered set

[:1,1:] is non empty Relation-like set

bool [:1,1:] is non empty set

[:[:1,1:],1:] is non empty Relation-like set

bool [:[:1,1:],1:] is non empty set

[:[:1,1:],REAL:] is non empty Relation-like set

bool [:[:1,1:],REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is non empty Relation-like set

bool [:[:REAL,REAL:],REAL:] is non empty set

2 is non empty natural V11() real ext-real positive non negative V172() V173() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

[:2,2:] is non empty Relation-like set

[:[:2,2:],REAL:] is non empty Relation-like set

bool [:[:2,2:],REAL:] is non empty set

K551() is V237() real-membered L18()

0 is empty trivial natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding V172() V173() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of NAT

Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like real-membered SubSpace of R^1

the carrier of (Closed-Interval-TSpace (0,1)) is non empty complex-membered ext-real-membered real-membered set

TOP-REAL 2 is non empty TopSpace-like V98() V123() V124() V125() V126() V127() V128() V129() V215() V216() V257() L19()

the carrier of (TOP-REAL 2) is non empty set

NonZero (TOP-REAL 2) is Element of bool the carrier of (TOP-REAL 2)

bool the carrier of (TOP-REAL 2) is non empty set

[#] (TOP-REAL 2) is non empty non proper open closed Element of bool the carrier of (TOP-REAL 2)

K164((TOP-REAL 2)) is Relation-like Function-like V39(2) FinSequence-like V55( TOP-REAL 2) V195() Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

{K164((TOP-REAL 2))} is non empty trivial set

([#] (TOP-REAL 2)) \ {K164((TOP-REAL 2))} is Element of bool the carrier of (TOP-REAL 2)

[:(NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)):] is Relation-like set

bool [:(NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)):] is non empty set

[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] is non empty Relation-like set

bool [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] is non empty set

K638(K551()) is TopStruct

the carrier of K638(K551()) is set

bool the carrier of K638(K551()) is non empty set

[.0,1.] is complex-membered ext-real-membered real-membered Element of bool REAL

0[01] is V11() real ext-real Element of the carrier of I[01]

1[01] is V11() real ext-real Element of the carrier of I[01]

(#) (0,1) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

(0,1) (#) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set

bool the carrier of I[01] is non empty set

1 / 2 is V11() real ext-real non negative Element of REAL

[:I[01],I[01]:] is non empty strict TopSpace-like T_0 T_1 T_2 compact TopStruct

the carrier of [:I[01],I[01]:] is non empty set

{ b

{ b

{ b

{ b

[:R^1,R^1:] is non empty strict TopSpace-like TopStruct

the carrier of [:R^1,R^1:] is non empty set

[: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):] is non empty Relation-like set

bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):] is non empty set

1 / 2 is V11() real ext-real non negative set

F

T is set

T is set

T is Relation-like Function-like set

proj1 T is set

T is Relation-like Function-like set

proj1 T is set

a is Element of F

T . a is set

F

F

F

[:[.0,1.],[.0,1.]:] is Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]

T is V11() real ext-real set

b is V11() real ext-real set

a is V11() real ext-real set

b - T is V11() real ext-real set

a - T is V11() real ext-real set

(b - T) / (a - T) is V11() real ext-real set

T is V11() real ext-real Element of the carrier of I[01]

2 * T is V11() real ext-real Element of REAL

2 * (1 / 2) is V11() real ext-real non negative Element of REAL

T is V11() real ext-real Element of the carrier of I[01]

2 * T is V11() real ext-real Element of REAL

(2 * T) - 1 is V11() real ext-real Element of REAL

2 * 1 is V11() real ext-real non negative Element of REAL

2 - 1 is V11() real ext-real Element of REAL

2 * (1 / 2) is V11() real ext-real non negative Element of REAL

1 - 1 is V11() real ext-real Element of REAL

T is V11() real ext-real Element of the carrier of I[01]

a is V11() real ext-real Element of the carrier of I[01]

T * a is V11() real ext-real set

T is V11() real ext-real Element of the carrier of I[01]

(1 / 2) * T is V11() real ext-real Element of REAL

(1 / 2) * 1 is V11() real ext-real non negative Element of REAL

4 is non empty natural V11() real ext-real positive non negative V172() V173() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

1 / 4 is V11() real ext-real non negative Element of REAL

T is V11() real ext-real Element of the carrier of I[01]

T - (1 / 4) is V11() real ext-real Element of REAL

1 + (1 / 4) is non empty V11() real ext-real positive non negative Element of REAL

(1 / 4) + 0 is V11() real ext-real non negative Element of REAL

id I[01] is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like V43( the carrier of I[01]) quasi_total continuous being_homeomorphism V171( I[01] , I[01] ) Element of bool [: the carrier of I[01], the carrier of I[01]:]

[: the carrier of I[01], the carrier of I[01]:] is non empty Relation-like set

bool [: the carrier of I[01], the carrier of I[01]:] is non empty set

id the carrier of I[01] is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued V43( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of I[01]:]

(id I[01]) . 0 is set

(id I[01]) . 1 is set

bool the carrier of [:I[01],I[01]:] is non empty set

T is V11() real ext-real Element of the carrier of I[01]

a is V11() real ext-real Element of the carrier of I[01]

b is V11() real ext-real Element of the carrier of I[01]

P is V11() real ext-real Element of the carrier of I[01]

[.T,a.] is complex-membered ext-real-membered real-membered Element of bool REAL

[.b,P.] is complex-membered ext-real-membered real-membered Element of bool REAL

[:[.T,a.],[.b,P.]:] is Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]

Q is non empty Element of bool the carrier of [:I[01],I[01]:]

{ b

AffineMap (1,0,(1 / 2),(1 / 2)) is non empty Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of (TOP-REAL 2)) quasi_total continuous Element of bool [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):]

Q is Element of bool the carrier of (TOP-REAL 2)

e2 is Element of bool the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(1 / 2))) .: Q is Element of bool the carrier of (TOP-REAL 2)

gg is set

dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)

gg is set

(AffineMap (1,0,(1 / 2),(1 / 2))) . gg is set

S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

S2 `2 is V11() real ext-real Element of REAL

K599(S2,2) is V11() real ext-real Element of REAL

S2 `1 is V11() real ext-real Element of REAL

K599(S2,1) is V11() real ext-real Element of REAL

2 * (S2 `1) is V11() real ext-real Element of REAL

(2 * (S2 `1)) - 1 is V11() real ext-real Element of REAL

(AffineMap (1,0,(1 / 2),(1 / 2))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

1 * (S2 `1) is V11() real ext-real Element of REAL

(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL

(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL

((1 / 2) * (S2 `2)) + (1 / 2) is V11() real ext-real Element of REAL

|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (1 / 2))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `1 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),1) is V11() real ext-real Element of REAL

((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),2) is V11() real ext-real Element of REAL

(1 / 2) * ((2 * (S2 `1)) - 1) is V11() real ext-real Element of REAL

(S2 `1) - (1 / 2) is V11() real ext-real Element of REAL

((S2 `1) - (1 / 2)) + (1 / 2) is V11() real ext-real Element of REAL

gg is set

rng (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)

dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)

gg is set

(AffineMap (1,0,(1 / 2),(1 / 2))) . gg is set

S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(1 / 2))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

S2 `1 is V11() real ext-real Element of REAL

K599(S2,1) is V11() real ext-real Element of REAL

1 * (S2 `1) is V11() real ext-real Element of REAL

(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL

S2 `2 is V11() real ext-real Element of REAL

K599(S2,2) is V11() real ext-real Element of REAL

(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL

((1 / 2) * (S2 `2)) + (1 / 2) is V11() real ext-real Element of REAL

|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (1 / 2))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `1 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),1) is V11() real ext-real Element of REAL

((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),2) is V11() real ext-real Element of REAL

2 * (((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2) is V11() real ext-real Element of REAL

2 * (S2 `1) is V11() real ext-real Element of REAL

g is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

g `2 is V11() real ext-real Element of REAL

K599(g,2) is V11() real ext-real Element of REAL

g `1 is V11() real ext-real Element of REAL

K599(g,1) is V11() real ext-real Element of REAL

(2 * (((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2)) - 1 is V11() real ext-real Element of REAL

(2 * (S2 `1)) - 1 is V11() real ext-real Element of REAL

{ b

Q is Element of bool the carrier of (TOP-REAL 2)

e2 is Element of bool the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(1 / 2))) .: Q is Element of bool the carrier of (TOP-REAL 2)

gg is set

dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)

gg is set

(AffineMap (1,0,(1 / 2),(1 / 2))) . gg is set

S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

S2 `1 is V11() real ext-real Element of REAL

K599(S2,1) is V11() real ext-real Element of REAL

2 * (S2 `1) is V11() real ext-real Element of REAL

(2 * (S2 `1)) - 1 is V11() real ext-real Element of REAL

S2 `2 is V11() real ext-real Element of REAL

K599(S2,2) is V11() real ext-real Element of REAL

(1 / 2) * ((2 * (S2 `1)) - 1) is V11() real ext-real Element of REAL

(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL

(AffineMap (1,0,(1 / 2),(1 / 2))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

1 * (S2 `1) is V11() real ext-real Element of REAL

(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL

((1 / 2) * (S2 `2)) + (1 / 2) is V11() real ext-real Element of REAL

|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (1 / 2))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `1 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),1) is V11() real ext-real Element of REAL

((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),2) is V11() real ext-real Element of REAL

(S2 `1) - (1 / 2) is V11() real ext-real Element of REAL

((S2 `1) - (1 / 2)) + (1 / 2) is V11() real ext-real Element of REAL

gg is set

rng (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)

dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)

gg is set

(AffineMap (1,0,(1 / 2),(1 / 2))) . gg is set

S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(1 / 2))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

S2 `1 is V11() real ext-real Element of REAL

K599(S2,1) is V11() real ext-real Element of REAL

1 * (S2 `1) is V11() real ext-real Element of REAL

(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL

S2 `2 is V11() real ext-real Element of REAL

K599(S2,2) is V11() real ext-real Element of REAL

(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL

((1 / 2) * (S2 `2)) + (1 / 2) is V11() real ext-real Element of REAL

|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (1 / 2))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `1 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),1) is V11() real ext-real Element of REAL

2 * (S2 `1) is V11() real ext-real Element of REAL

((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(1 / 2))) . S2),2) is V11() real ext-real Element of REAL

2 * (((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2) is V11() real ext-real Element of REAL

g is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

g `1 is V11() real ext-real Element of REAL

K599(g,1) is V11() real ext-real Element of REAL

g `2 is V11() real ext-real Element of REAL

K599(g,2) is V11() real ext-real Element of REAL

(2 * (S2 `1)) - 1 is V11() real ext-real Element of REAL

(2 * (((AffineMap (1,0,(1 / 2),(1 / 2))) . S2) `2)) - 1 is V11() real ext-real Element of REAL

{ b

- (1 / 2) is V11() real ext-real non positive Element of REAL

AffineMap (1,0,(1 / 2),(- (1 / 2))) is non empty Relation-like the carrier of (TOP-REAL 2) -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of (TOP-REAL 2)) quasi_total continuous Element of bool [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):]

Q is Element of bool the carrier of (TOP-REAL 2)

e2 is Element of bool the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: Q is Element of bool the carrier of (TOP-REAL 2)

gg is set

dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)

gg is set

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . gg is set

S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

S2 `1 is V11() real ext-real Element of REAL

K599(S2,1) is V11() real ext-real Element of REAL

2 * (S2 `1) is V11() real ext-real Element of REAL

1 - (2 * (S2 `1)) is V11() real ext-real Element of REAL

S2 `2 is V11() real ext-real Element of REAL

K599(S2,2) is V11() real ext-real Element of REAL

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

(1 / 2) * (1 - (2 * (S2 `1))) is V11() real ext-real Element of REAL

(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL

(1 / 2) - (S2 `1) is V11() real ext-real Element of REAL

((1 / 2) - (S2 `1)) + (- (1 / 2)) is V11() real ext-real Element of REAL

((1 / 2) * (S2 `2)) + (- (1 / 2)) is V11() real ext-real Element of REAL

1 * (S2 `1) is V11() real ext-real Element of REAL

(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL

|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (- (1 / 2)))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `1 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),1) is V11() real ext-real Element of REAL

- (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `1) is V11() real ext-real Element of REAL

((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),2) is V11() real ext-real Element of REAL

gg is set

rng (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)

dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)

gg is set

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . gg is set

S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

S2 `1 is V11() real ext-real Element of REAL

K599(S2,1) is V11() real ext-real Element of REAL

1 * (S2 `1) is V11() real ext-real Element of REAL

(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL

S2 `2 is V11() real ext-real Element of REAL

K599(S2,2) is V11() real ext-real Element of REAL

(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL

((1 / 2) * (S2 `2)) + (- (1 / 2)) is V11() real ext-real Element of REAL

|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (- (1 / 2)))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `1 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),1) is V11() real ext-real Element of REAL

- (S2 `1) is V11() real ext-real Element of REAL

2 * (- (S2 `1)) is V11() real ext-real Element of REAL

((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),2) is V11() real ext-real Element of REAL

2 * (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2) is V11() real ext-real Element of REAL

g is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

g `1 is V11() real ext-real Element of REAL

K599(g,1) is V11() real ext-real Element of REAL

- (g `1) is V11() real ext-real Element of REAL

g `2 is V11() real ext-real Element of REAL

K599(g,2) is V11() real ext-real Element of REAL

(2 * (- (S2 `1))) + 1 is V11() real ext-real Element of REAL

(2 * (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2)) + 1 is V11() real ext-real Element of REAL

2 * (S2 `1) is V11() real ext-real Element of REAL

1 - (2 * (S2 `1)) is V11() real ext-real Element of REAL

{ b

Q is Element of bool the carrier of (TOP-REAL 2)

e2 is Element of bool the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: Q is Element of bool the carrier of (TOP-REAL 2)

gg is set

dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)

gg is set

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . gg is set

S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

S2 `2 is V11() real ext-real Element of REAL

K599(S2,2) is V11() real ext-real Element of REAL

S2 `1 is V11() real ext-real Element of REAL

K599(S2,1) is V11() real ext-real Element of REAL

2 * (S2 `1) is V11() real ext-real Element of REAL

1 - (2 * (S2 `1)) is V11() real ext-real Element of REAL

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL

(1 / 2) * (1 - (2 * (S2 `1))) is V11() real ext-real Element of REAL

((1 / 2) * (S2 `2)) + (- (1 / 2)) is V11() real ext-real Element of REAL

(1 / 2) - (S2 `1) is V11() real ext-real Element of REAL

((1 / 2) - (S2 `1)) + (- (1 / 2)) is V11() real ext-real Element of REAL

1 * (S2 `1) is V11() real ext-real Element of REAL

(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL

|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (- (1 / 2)))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `1 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),1) is V11() real ext-real Element of REAL

((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),2) is V11() real ext-real Element of REAL

- (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `1) is V11() real ext-real Element of REAL

gg is set

rng (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)

dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)

gg is set

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . gg is set

S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

S2 `1 is V11() real ext-real Element of REAL

K599(S2,1) is V11() real ext-real Element of REAL

1 * (S2 `1) is V11() real ext-real Element of REAL

(1 * (S2 `1)) + 0 is V11() real ext-real Element of REAL

S2 `2 is V11() real ext-real Element of REAL

K599(S2,2) is V11() real ext-real Element of REAL

(1 / 2) * (S2 `2) is V11() real ext-real Element of REAL

((1 / 2) * (S2 `2)) + (- (1 / 2)) is V11() real ext-real Element of REAL

|[((1 * (S2 `1)) + 0),(((1 / 2) * (S2 `2)) + (- (1 / 2)))]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `1 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),1) is V11() real ext-real Element of REAL

((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2 is V11() real ext-real Element of REAL

K599(((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2),2) is V11() real ext-real Element of REAL

2 * (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2) is V11() real ext-real Element of REAL

- (S2 `1) is V11() real ext-real Element of REAL

2 * (- (S2 `1)) is V11() real ext-real Element of REAL

g is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

g `2 is V11() real ext-real Element of REAL

K599(g,2) is V11() real ext-real Element of REAL

g `1 is V11() real ext-real Element of REAL

K599(g,1) is V11() real ext-real Element of REAL

- (g `1) is V11() real ext-real Element of REAL

(2 * (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . S2) `2)) + 1 is V11() real ext-real Element of REAL

(2 * (- (S2 `1))) + 1 is V11() real ext-real Element of REAL

2 * (S2 `1) is V11() real ext-real Element of REAL

1 - (2 * (S2 `1)) is V11() real ext-real Element of REAL

T is non empty 1-sorted

the carrier of T is non empty set

a is Element of the carrier of T

a is set

T is real-membered 1-sorted

the carrier of T is complex-membered ext-real-membered real-membered set

a is V11() real ext-real Element of the carrier of T

T is real-membered TopStruct

a is real-membered SubSpace of T

T is non empty TopSpace-like real-membered TopStruct

a is non empty TopSpace-like real-membered TopStruct

[:T,a:] is non empty strict TopSpace-like TopStruct

the carrier of [:T,a:] is non empty set

b is Element of the carrier of [:T,a:]

b `1 is set

the carrier of T is non empty complex-membered ext-real-membered real-membered set

the carrier of a is non empty complex-membered ext-real-membered real-membered set

[: the carrier of T, the carrier of a:] is non empty Relation-like set

b `2 is set

the carrier of T is non empty complex-membered ext-real-membered real-membered set

the carrier of a is non empty complex-membered ext-real-membered real-membered set

[: the carrier of T, the carrier of a:] is non empty Relation-like set

T is non empty TopSpace-like T_0 T_1 T_2 SubSpace of [:I[01],I[01]:]

the carrier of T is non empty set

a is Element of the carrier of T

a `1 is set

b is Element of the carrier of [:I[01],I[01]:]

b `1 is V11() real ext-real set

a `2 is set

b is Element of the carrier of [:I[01],I[01]:]

b `2 is V11() real ext-real set

{ b

b is Element of bool the carrier of (TOP-REAL 2)

dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(1 / 2))) .: b is Element of bool the carrier of (TOP-REAL 2)

T is closed Element of bool the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(1 / 2))) " ((AffineMap (1,0,(1 / 2),(1 / 2))) .: b) is Element of bool the carrier of (TOP-REAL 2)

{ b

b is Element of bool the carrier of (TOP-REAL 2)

dom (AffineMap (1,0,(1 / 2),(1 / 2))) is non empty Element of bool the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(1 / 2))) .: b is Element of bool the carrier of (TOP-REAL 2)

T is closed Element of bool the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(1 / 2))) " ((AffineMap (1,0,(1 / 2),(1 / 2))) .: b) is Element of bool the carrier of (TOP-REAL 2)

{ b

b is Element of bool the carrier of (TOP-REAL 2)

dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: b is Element of bool the carrier of (TOP-REAL 2)

T is closed Element of bool the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) " ((AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: b) is Element of bool the carrier of (TOP-REAL 2)

{ b

b is Element of bool the carrier of (TOP-REAL 2)

dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) is non empty Element of bool the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: b is Element of bool the carrier of (TOP-REAL 2)

T is closed Element of bool the carrier of (TOP-REAL 2)

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) " ((AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: b) is Element of bool the carrier of (TOP-REAL 2)

{ b

{ b

{ b

{ b

{ b

a is closed Element of bool the carrier of (TOP-REAL 2)

T is closed Element of bool the carrier of (TOP-REAL 2)

a /\ T is closed Element of bool the carrier of (TOP-REAL 2)

REAL 2 is non empty FinSequence-membered FinSequenceSet of REAL

2 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

T is V11() real ext-real Element of REAL

a is V11() real ext-real Element of REAL

<*T,a*> is set

[:NAT,REAL:] is Relation-like set

bool [:NAT,REAL:] is non empty set

[:[:REAL,REAL:],(REAL 2):] is non empty Relation-like set

bool [:[:REAL,REAL:],(REAL 2):] is non empty set

T is non empty Relation-like [:REAL,REAL:] -defined REAL 2 -valued Function-like V43([:REAL,REAL:]) quasi_total Element of bool [:[:REAL,REAL:],(REAL 2):]

[: the carrier of R^1, the carrier of R^1:] is non empty Relation-like set

a is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of [:R^1,R^1:]) quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

b is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

[b,P] is non empty V29() set

{b,P} is non empty complex-membered ext-real-membered real-membered set

{b} is non empty trivial complex-membered ext-real-membered real-membered set

{{b,P},{b}} is non empty set

a . [b,P] is set

<*b,P*> is set

a . (b,P) is set

Q is Relation-like NAT -defined REAL -valued Function-like V39(2) FinSequence-like Element of REAL 2

b is V11() real ext-real Element of REAL

P is V11() real ext-real Element of REAL

[b,P] is non empty V29() set

{b,P} is non empty complex-membered ext-real-membered real-membered set

{b} is non empty trivial complex-membered ext-real-membered real-membered set

{{b,P},{b}} is non empty set

a . [b,P] is set

<*b,P*> is set

{ b

bool the carrier of [:R^1,R^1:] is non empty set

{ b

{ b

Q is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of [:R^1,R^1:]) quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

Q is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of [:R^1,R^1:]) quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

P is Element of bool the carrier of (TOP-REAL 2)

b is Element of bool the carrier of [:R^1,R^1:]

Q .: b is Element of bool the carrier of (TOP-REAL 2)

Q is set

e2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

e2 `2 is V11() real ext-real Element of REAL

K599(e2,2) is V11() real ext-real Element of REAL

e2 `1 is V11() real ext-real Element of REAL

K599(e2,1) is V11() real ext-real Element of REAL

2 * (e2 `1) is V11() real ext-real Element of REAL

1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL

REAL 2 is non empty FinSequence-membered FinSequenceSet of REAL

2 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

gg is V11() real ext-real Element of REAL

gg is V11() real ext-real Element of REAL

<*gg,gg*> is set

2 * gg is V11() real ext-real Element of REAL

1 - (2 * gg) is V11() real ext-real Element of REAL

[gg,gg] is non empty V29() set

{gg,gg} is non empty complex-membered ext-real-membered real-membered set

{gg} is non empty trivial complex-membered ext-real-membered real-membered set

{{gg,gg},{gg}} is non empty set

g is Element of the carrier of [:R^1,R^1:]

dom Q is non empty Element of bool the carrier of [:R^1,R^1:]

g `1 is V11() real ext-real set

g `2 is V11() real ext-real set

Q . g is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

Q is set

dom Q is non empty Element of bool the carrier of [:R^1,R^1:]

e2 is set

Q . e2 is set

gg is Element of the carrier of [:R^1,R^1:]

gg `2 is V11() real ext-real set

gg `1 is V11() real ext-real set

2 * (gg `1) is V11() real ext-real Element of REAL

1 - (2 * (gg `1)) is V11() real ext-real Element of REAL

[: the carrier of R^1, the carrier of R^1:] is non empty Relation-like set

gg is set

S2 is set

[gg,S2] is non empty V29() set

{gg,S2} is non empty set

{gg} is non empty trivial set

{{gg,S2},{gg}} is non empty set

g is V11() real ext-real Element of REAL

g is V11() real ext-real Element of REAL

|[g,g]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

S3 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

S3 `1 is V11() real ext-real Element of REAL

K599(S3,1) is V11() real ext-real Element of REAL

S3 `2 is V11() real ext-real Element of REAL

K599(S3,2) is V11() real ext-real Element of REAL

{ b

{ b

{ b

Q is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of [:R^1,R^1:]) quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

Q is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of [:R^1,R^1:]) quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

P is Element of bool the carrier of (TOP-REAL 2)

b is Element of bool the carrier of [:R^1,R^1:]

Q .: b is Element of bool the carrier of (TOP-REAL 2)

Q is set

e2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

e2 `2 is V11() real ext-real Element of REAL

K599(e2,2) is V11() real ext-real Element of REAL

e2 `1 is V11() real ext-real Element of REAL

K599(e2,1) is V11() real ext-real Element of REAL

2 * (e2 `1) is V11() real ext-real Element of REAL

(2 * (e2 `1)) - 1 is V11() real ext-real Element of REAL

REAL 2 is non empty FinSequence-membered FinSequenceSet of REAL

2 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

gg is V11() real ext-real Element of REAL

gg is V11() real ext-real Element of REAL

<*gg,gg*> is set

2 * gg is V11() real ext-real Element of REAL

(2 * gg) - 1 is V11() real ext-real Element of REAL

[gg,gg] is non empty V29() set

{gg,gg} is non empty complex-membered ext-real-membered real-membered set

{gg} is non empty trivial complex-membered ext-real-membered real-membered set

{{gg,gg},{gg}} is non empty set

[: the carrier of R^1, the carrier of R^1:] is non empty Relation-like set

g is Element of the carrier of [:R^1,R^1:]

dom Q is non empty Element of bool the carrier of [:R^1,R^1:]

g `1 is V11() real ext-real set

g `2 is V11() real ext-real set

Q . g is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

Q is set

dom Q is non empty Element of bool the carrier of [:R^1,R^1:]

e2 is set

Q . e2 is set

gg is Element of the carrier of [:R^1,R^1:]

gg `2 is V11() real ext-real set

gg `1 is V11() real ext-real set

2 * (gg `1) is V11() real ext-real Element of REAL

(2 * (gg `1)) - 1 is V11() real ext-real Element of REAL

[: the carrier of R^1, the carrier of R^1:] is non empty Relation-like set

gg is set

S2 is set

[gg,S2] is non empty V29() set

{gg,S2} is non empty set

{gg} is non empty trivial set

{{gg,S2},{gg}} is non empty set

g is V11() real ext-real Element of REAL

g is V11() real ext-real Element of REAL

|[g,g]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

S3 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

S3 `1 is V11() real ext-real Element of REAL

K599(S3,1) is V11() real ext-real Element of REAL

S3 `2 is V11() real ext-real Element of REAL

K599(S3,2) is V11() real ext-real Element of REAL

{ b

{ b

{ b

Q is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of [:R^1,R^1:]) quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

Q is non empty Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like V43( the carrier of [:R^1,R^1:]) quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]

P is Element of bool the carrier of (TOP-REAL 2)

b is Element of bool the carrier of [:R^1,R^1:]

Q .: b is Element of bool the carrier of (TOP-REAL 2)

Q is set

e2 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

e2 `1 is V11() real ext-real Element of REAL

K599(e2,1) is V11() real ext-real Element of REAL

2 * (e2 `1) is V11() real ext-real Element of REAL

1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL

e2 `2 is V11() real ext-real Element of REAL

K599(e2,2) is V11() real ext-real Element of REAL

(2 * (e2 `1)) - 1 is V11() real ext-real Element of REAL

REAL 2 is non empty FinSequence-membered FinSequenceSet of REAL

2 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

gg is V11() real ext-real Element of REAL

gg is V11() real ext-real Element of REAL

<*gg,gg*> is set

2 * gg is V11() real ext-real Element of REAL

1 - (2 * gg) is V11() real ext-real Element of REAL

(2 * gg) - 1 is V11() real ext-real Element of REAL

[gg,gg] is non empty V29() set

{gg,gg} is non empty complex-membered ext-real-membered real-membered set

{gg} is non empty trivial complex-membered ext-real-membered real-membered set

{{gg,gg},{gg}} is non empty set

[: the carrier of R^1, the carrier of R^1:] is non empty Relation-like set

g is Element of the carrier of [:R^1,R^1:]

dom Q is non empty Element of bool the carrier of [:R^1,R^1:]

g `1 is V11() real ext-real set

g `2 is V11() real ext-real set

Q . g is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

Q is set

dom Q is non empty Element of bool the carrier of [:R^1,R^1:]

e2 is set

Q . e2 is set

gg is Element of the carrier of [:R^1,R^1:]

gg `1 is V11() real ext-real set

2 * (gg `1) is V11() real ext-real Element of REAL

1 - (2 * (gg `1)) is V11() real ext-real Element of REAL

gg `2 is V11() real ext-real set

(2 * (gg `1)) - 1 is V11() real ext-real Element of REAL

[: the carrier of R^1, the carrier of R^1:] is non empty Relation-like set

gg is set

S2 is set

[gg,S2] is non empty V29() set

{gg,S2} is non empty set

{gg} is non empty trivial set

{{gg,S2},{gg}} is non empty set

g is V11() real ext-real Element of REAL

g is V11() real ext-real Element of REAL

|[g,g]| is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

S3 is Relation-like Function-like V39(2) FinSequence-like V195() Element of the carrier of (TOP-REAL 2)

S3 `1 is V11() real ext-real Element of REAL

K599(S3,1) is V11() real ext-real Element of REAL

S3 `2 is V11() real ext-real Element of REAL

K599(S3,2) is V11() real ext-real Element of REAL

{ b

[0,0] is non empty V29() set

{0,0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

{0} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

{{0,0},{0}} is non empty set

P is closed Element of bool the carrier of [:R^1,R^1:]

[#] [:I[01],I[01]:] is non empty non proper open closed Element of bool the carrier of [:I[01],I[01]:]

P /\ ([#] [:I[01],I[01]:]) is Element of bool the carrier of [:I[01],I[01]:]

Q is set

e2 is Element of the carrier of [:I[01],I[01]:]

e2 `2 is V11() real ext-real set

e2 `1 is V11() real ext-real set

2 * (e2 `1) is V11() real ext-real Element of REAL

1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL

e2 is Element of the carrier of [:R^1,R^1:]

e2 `2 is V11() real ext-real set

e2 `1 is V11() real ext-real set

2 * (e2 `1) is V11() real ext-real Element of REAL

1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL

gg is Element of the carrier of [:I[01],I[01]:]

gg `2 is V11() real ext-real set

gg `1 is V11() real ext-real set

2 * (gg `1) is V11() real ext-real Element of REAL

1 - (2 * (gg `1)) is V11() real ext-real Element of REAL

gg is Element of the carrier of [:I[01],I[01]:]

gg `2 is V11() real ext-real set

gg `1 is V11() real ext-real set

2 * (gg `1) is V11() real ext-real Element of REAL

1 - (2 * (gg `1)) is V11() real ext-real Element of REAL

Q is set

e2 is Element of the carrier of [:R^1,R^1:]

e2 `2 is V11() real ext-real set

e2 `1 is V11() real ext-real set

2 * (e2 `1) is V11() real ext-real Element of REAL

1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL

b is Element of the carrier of [:I[01],I[01]:]

b `1 is V11() real ext-real set

b `2 is V11() real ext-real set

2 * (b `1) is V11() real ext-real Element of REAL

1 - (2 * (b `1)) is V11() real ext-real Element of REAL

{ b

[1,1] is non empty V29() set

{1,1} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

{1} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

{{1,1},{1}} is non empty set

b is Element of the carrier of [:I[01],I[01]:]

b `1 is V11() real ext-real set

2 * (b `1) is V11() real ext-real Element of REAL

(2 * (b `1)) - 1 is V11() real ext-real Element of REAL

b `2 is V11() real ext-real set

P is closed Element of bool the carrier of [:R^1,R^1:]

[#] [:I[01],I[01]:] is non empty non proper open closed Element of bool the carrier of [:I[01],I[01]:]

P /\ ([#] [:I[01],I[01]:]) is Element of bool the carrier of [:I[01],I[01]:]

Q is set

e2 is Element of the carrier of [:I[01],I[01]:]

e2 `1 is V11() real ext-real set

2 * (e2 `1) is V11() real ext-real Element of REAL

1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL

e2 `2 is V11() real ext-real set

(2 * (e2 `1)) - 1 is V11() real ext-real Element of REAL

e2 is Element of the carrier of [:R^1,R^1:]

e2 `1 is V11() real ext-real set

2 * (e2 `1) is V11() real ext-real Element of REAL

1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL

e2 `2 is V11() real ext-real set

gg is Element of the carrier of [:I[01],I[01]:]

gg `1 is V11() real ext-real set

2 * (gg `1) is V11() real ext-real Element of REAL

1 - (2 * (gg `1)) is V11() real ext-real Element of REAL

gg `2 is V11() real ext-real set

(2 * (gg `1)) - 1 is V11() real ext-real Element of REAL

gg is Element of the carrier of [:I[01],I[01]:]

gg `1 is V11() real ext-real set

2 * (gg `1) is V11() real ext-real Element of REAL

1 - (2 * (gg `1)) is V11() real ext-real Element of REAL

gg `2 is V11() real ext-real set

(2 * (gg `1)) - 1 is V11() real ext-real Element of REAL

gg is Element of the carrier of [:I[01],I[01]:]

gg `1 is V11() real ext-real set

2 * (gg `1) is V11() real ext-real Element of REAL

1 - (2 * (gg `1)) is V11() real ext-real Element of REAL

gg `2 is V11() real ext-real set

(2 * (gg `1)) - 1 is V11() real ext-real Element of REAL

Q is set

e2 is Element of the carrier of [:R^1,R^1:]

e2 `1 is V11() real ext-real set

2 * (e2 `1) is V11() real ext-real Element of REAL

1 - (2 * (e2 `1)) is V11() real ext-real Element of REAL

e2 `2 is V11() real ext-real set

(2 * (e2 `1)) - 1 is V11() real ext-real Element of REAL

1 - (2 * (b `1)) is V11() real ext-real Element of REAL

{ b

[1,0] is non empty V29() set

{1,0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

{1} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

{{1,0},{1}} is non empty set

P is closed Element of bool the carrier of [:R^1,R^1:]

[#] [:I[01],I[01]:] is non empty non proper open closed Element of bool the carrier of [:I[01],I[01]:]

P /\ ([#] [:I[01],I[01]:]) is Element of bool the carrier of [:I[01],I[01]:]

Q is set

e2 is Element of the carrier of [:I[01],I[01]:]

e2 `2 is V11() real ext-real set

e2 `1 is V11() real ext-real set

2 * (e2 `1) is V11() real ext-real Element of REAL

(2 * (e2 `1)) - 1 is V11() real ext-real Element of REAL

e2 is Element of the carrier of [:R^1,R^1:]

e2 `2 is V11() real ext-real set

e2 `1 is V11() real ext-real set

2 * (e2 `1) is V11() real ext-real Element of REAL

(2 * (e2 `1)) - 1 is V11() real ext-real Element of REAL

gg is Element of the carrier of [:I[01],I[01]:]

gg `2 is V11() real ext-real set

gg `1 is V11() real ext-real set

2 * (gg `1) is V11() real ext-real Element of REAL

(2 * (gg `1)) - 1 is V11() real ext-real Element of REAL

gg is Element of the carrier of [:I[01],I[01]:]

gg `2 is V11() real ext-real set

gg `1 is V11() real ext-real set

2 * (gg `1) is V11() real ext-real Element of REAL

(2 * (gg `1)) - 1 is V11() real ext-real Element of REAL

Q is set

e2 is Element of the carrier of [:R^1,R^1:]

e2 `2 is V11() real ext-real set

e2 `1 is V11() real ext-real set

2 * (e2 `1) is V11() real ext-real Element of REAL

(2 * (e2 `1)) - 1 is V11() real ext-real Element of REAL

b is Element of the carrier of [:I[01],I[01]:]

b `1 is V11() real ext-real set

b `2 is V11() real ext-real set

2 * (b `1) is V11() real ext-real Element of REAL

(2 * (b `1)) - 1 is V11() real ext-real Element of REAL

T is non empty TopSpace-like TopStruct

a is non empty TopSpace-like TopStruct

[:T,a:] is non empty strict TopSpace-like TopStruct

the carrier of [:T,a:] is non empty set

the carrier of T is non empty set

the carrier of a is non empty set

b is Element of the carrier of [:T,a:]

b `1 is set

b `2 is set

[: the carrier of T, the carrier of a:] is non empty Relation-like set

[.0,(1 / 2).] is complex-membered ext-real-membered real-membered Element of bool REAL

[:[.0,(1 / 2).],[.0,1.]:] is Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]

[.(1 / 2),1.] is complex-membered ext-real-membered real-membered Element of bool REAL

[:[.(1 / 2),1.],[.0,1.]:] is Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]

[#] [:I[01],I[01]:] is non empty non proper open closed Element of bool the carrier of [:I[01],I[01]:]

T is Element of bool the carrier of [:I[01],I[01]:]

a is Element of bool the carrier of [:I[01],I[01]:]

[:I[01],I[01]:] | T is strict TopSpace-like T_0 T_1 T_2 SubSpace of [:I[01],I[01]:]

[#] ([:I[01],I[01]:] | T) is non proper open closed Element of bool the carrier of ([:I[01],I[01]:] | T)

the carrier of ([:I[01],I[01]:] | T) is set

bool the carrier of ([:I[01],I[01]:] | T) is non empty set

[:I[01],I[01]:] | a is strict TopSpace-like T_0 T_1 T_2 SubSpace of [:I[01],I[01]:]

[#] ([:I[01],I[01]:] | a) is non proper open closed Element of bool the carrier of ([:I[01],I[01]:] | a)

the carrier of ([:I[01],I[01]:] | a) is set

bool the carrier of ([:I[01],I[01]:] | a) is non empty set

([#] ([:I[01],I[01]:] | T)) \/ ([#] ([:I[01],I[01]:] | a)) is set

T \/ ([#] ([:I[01],I[01]:] | a)) is set

T \/ a is Element of bool the carrier of [:I[01],I[01]:]

[.0,(1 / 2).] \/ [.(1 / 2),1.] is complex-membered ext-real-membered real-membered Element of bool REAL

[:([.0,(1 / 2).] \/ [.(1 / 2),1.]),[.0,1.]:] is Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]

{(1 / 2)} is non empty trivial complex-membered ext-real-membered real-membered set

[:{(1 / 2)},[.0,1.]:] is Relation-like set

T is Element of bool the carrier of [:I[01],I[01]:]

a is Element of bool the carrier of [:I[01],I[01]:]

[:I[01],I[01]:] | a is strict TopSpace-like T_0 T_1 T_2 SubSpace of [:I[01],I[01]:]

the carrier of ([:I[01],I[01]:] | a) is set

[:I[01],I[01]:] | T is strict TopSpace-like T_0 T_1 T_2 SubSpace of [:I[01],I[01]:]

[#] ([:I[01],I[01]:] | T) is non proper open closed Element of bool the carrier of ([:I[01],I[01]:] | T)

the carrier of ([:I[01],I[01]:] | T) is set

bool the carrier of ([:I[01],I[01]:] | T) is non empty set

[#] ([:I[01],I[01]:] | a) is non proper open closed Element of bool the carrier of ([:I[01],I[01]:] | a)

bool the carrier of ([:I[01],I[01]:] | a) is non empty set

([#] ([:I[01],I[01]:] | T)) /\ ([#] ([:I[01],I[01]:] | a)) is Element of bool the carrier of ([:I[01],I[01]:] | a)

T /\ ([#] ([:I[01],I[01]:] | a)) is Element of bool the carrier of ([:I[01],I[01]:] | a)

T /\ a is Element of bool the carrier of [:I[01],I[01]:]

[.0,(1 / 2).] /\ [.(1 / 2),1.] is complex-membered ext-real-membered real-membered Element of bool REAL

[:([.0,(1 / 2).] /\ [.(1 / 2),1.]),[.0,1.]:] is Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty set

{} T is empty trivial Relation-like non-empty empty-yielding compact complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool the carrier of T

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty set

{} T is empty trivial Relation-like non-empty empty-yielding compact complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool the carrier of T

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty set

a is V11() real ext-real set

b is V11() real ext-real set

[.a,b.] is complex-membered ext-real-membered real-membered Element of bool REAL

{} T is empty trivial Relation-like non-empty empty-yielding compact complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool the carrier of T

T is V11() real ext-real Element of the carrier of I[01]

a is V11() real ext-real Element of the carrier of I[01]

[.T,a.] is complex-membered ext-real-membered real-membered Element of bool REAL

b is V11() real ext-real Element of the carrier of I[01]

P is V11() real ext-real Element of the carrier of I[01]

[.b,P.] is complex-membered ext-real-membered real-membered Element of bool REAL

[:[.T,a.],[.b,P.]:] is Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]

Q is empty trivial proper Relation-like non-empty empty-yielding open closed compact complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool the carrier of I[01]

[:Q,[.b,P.]:] is empty trivial proper Relation-like non-empty empty-yielding the carrier of I[01] -defined REAL -valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool [: the carrier of I[01],REAL:]

[: the carrier of I[01],REAL:] is non empty Relation-like set

bool [: the carrier of I[01],REAL:] is non empty set

Q is empty trivial proper Relation-like non-empty empty-yielding open closed compact complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool the carrier of I[01]

[:[.T,a.],Q:] is empty trivial proper Relation-like non-empty empty-yielding REAL -defined the carrier of I[01] -valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool [:REAL, the carrier of I[01]:]

[:REAL, the carrier of I[01]:] is non empty Relation-like set

bool [:REAL, the carrier of I[01]:] is non empty set

Q is empty trivial proper Relation-like non-empty empty-yielding open closed compact complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool the carrier of I[01]

[:[.T,a.],Q:] is empty trivial proper Relation-like non-empty empty-yielding REAL -defined the carrier of I[01] -valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V209() Element of bool [:REAL, the carrier of I[01]:]

[:REAL, the carrier of I[01]:] is non empty Relation-like set

bool [:REAL, the carrier of I[01]:] is non empty set

T is V11() real ext-real set

a is V11() real ext-real set

Closed-Interval-TSpace (T,a) is non empty strict TopSpace-like real-membered SubSpace of R^1

the carrier of (Closed-Interval-TSpace (T,a)) is non empty complex-membered ext-real-membered real-membered set

b is V11() real ext-real set

P is V11() real ext-real set

Closed-Interval-TSpace (b,P) is non empty strict TopSpace-like real-membered SubSpace of R^1

the carrier of (Closed-Interval-TSpace (b,P)) is non empty complex-membered ext-real-membered real-membered set

P[01] (T,a,((#) (0,1)),((0,1) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,a)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like V43( the carrier of (Closed-Interval-TSpace (T,a))) quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (0,1)):]

[: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty Relation-like set

bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty set

(#) (b,P) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (b,P))

(b,P) (#) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (b,P))

L[01] (((#) (b,P)),((b,P) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (b,P)) -valued Function-like V43( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,P)):]

[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty Relation-like set

bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty set

(L[01] (((#) (b,P)),((b,P) (#)))) * (P[01] (T,a,((#) (0,1)),((0,1) (#)))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,a)) -defined the carrier of (Closed-Interval-TSpace (b,P)) -valued Function-like V43( the carrier of (Closed-Interval-TSpace (T,a))) quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (b,P)):]

[: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty Relation-like set

bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty set

a is V11() real ext-real set

T is V11() real ext-real set

P is V11() real ext-real set

b is V11() real ext-real set

(T,a,b,P) is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,a)) -defined the carrier of (Closed-Interval-TSpace (b,P)) -valued Function-like V43( the carrier of (Closed-Interval-TSpace (T,a))) quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (b,P)):]

Closed-Interval-TSpace (T,a) is non empty strict TopSpace-like real-membered SubSpace of R^1

the carrier of (Closed-Interval-TSpace (T,a)) is non empty complex-membered ext-real-membered real-membered set

Closed-Interval-TSpace (b,P) is non empty strict TopSpace-like real-membered SubSpace of R^1

the carrier of (Closed-Interval-TSpace (b,P)) is non empty complex-membered ext-real-membered real-membered set

[: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty Relation-like set

bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty set

P[01] (T,a,((#) (0,1)),((0,1) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,a)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like V43( the carrier of (Closed-Interval-TSpace (T,a))) quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (0,1)):]

[: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty Relation-like set

bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty set

(#) (b,P) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (b,P))

(b,P) (#) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (b,P))

L[01] (((#) (b,P)),((b,P) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (b,P)) -valued Function-like V43( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,P)):]

[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty Relation-like set

bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,P)):] is non empty set

(L[01] (((#) (b,P)),((b,P) (#)))) * (P[01] (T,a,((#) (0,1)),((0,1) (#)))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,a)) -defined the carrier of (Closed-Interval-TSpace (b,P)) -valued Function-like V43( the carrier of (Closed-Interval-TSpace (T,a))) quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (T,a)), the carrier of (Closed-Interval-TSpace (b,P)):]

(T,a,b,P) . T is set

(T,a,b,P) . a is set

[.T,a.] is complex-membered ext-real-membered real-membered Element of bool REAL

dom (P[01] (T,a,((#) (0,1)),((0,1) (#)))) is non empty complex-membered ext-real-membered real-membered Element of bool the carrier of (Closed-Interval-TSpace (T,a))

bool the carrier of (Closed-Interval-TSpace (T,a)) is non empty set

(P[01] (T,a,((#) (0,1)),((0,1) (#)))) . T is set

(L[01] (((#) (b,P)),((b,P) (#)))