:: BORSUK_2 semantic presentation

REAL is V33() V34() V35() V39() V138() V139() V141() set
NAT is V33() V34() V35() V36() V37() V38() V39() V138() Element of bool REAL
bool REAL is non empty set

1 is non empty natural V31() real V33() V34() V35() V36() V37() V38() ext-real positive V136() V138() Element of NAT
{{},1} is non empty set
omega is V33() V34() V35() V36() V37() V38() V39() V138() set
bool omega is non empty set
bool NAT is non empty set

the carrier of I[01] is non empty V33() V34() V35() 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

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

bool is non empty set
2 is non empty natural V31() real V33() V34() V35() V36() V37() V38() ext-real positive V136() V138() Element of NAT
[:2,2:] is non empty Relation-like set

bool [:[:2,2:],REAL:] is non empty set
K300() is non empty V116() V121() V122() V123() V124() V126() V130() L7()
R^1 is non empty strict TopSpace-like V130() TopStruct

Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V130() SubSpace of R^1
the carrier of () is non empty V33() V34() V35() set
COMPLEX is V33() V39() set
[.0,1.] is V33() V34() V35() V141() Element of bool REAL
0[01] is V31() real ext-real Element of the carrier of I[01]
1[01] is V31() real ext-real Element of the carrier of I[01]
(#) (0,1) is V31() real ext-real Element of the carrier of ()
(0,1) (#) is V31() real ext-real Element of the carrier of ()

I[01] is non empty strict TopSpace-like V130() SubSpace of R^1
the carrier of I[01] is non empty V33() V34() V35() set
bool the carrier of I[01] is non empty set
a is V31() real ext-real set
{ b1 where b1 is V31() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
b is V31() real ext-real Element of REAL
F1() is non empty set
F2() is set
{ F3(b1) where b1 is Element of F1() : ( b1 in F2() & P1[b1] ) } is set
card { F3(b1) where b1 is Element of F1() : ( b1 in F2() & P1[b1] ) } is cardinal set
card F2() is cardinal set

dom a is set
rng a is set
b is set
B is Element of F1()
F3(B) is set
a . B is set
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
[#] a is non empty non proper open closed dense non boundary Element of bool the carrier of a
bool the carrier of a is non empty set
b is non empty TopSpace-like TopStruct
the carrier of b is non empty set
[: the carrier of a, the carrier of b:] is non empty Relation-like set
bool [: the carrier of a, the carrier of b:] is non empty set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
[: the carrier of B, the carrier of b:] is non empty Relation-like set
bool [: the carrier of B, the carrier of b:] is non empty set
[#] B is non empty non proper open closed dense non boundary Element of bool the carrier of B
bool the carrier of B is non empty set
([#] a) \/ ([#] B) is non empty set
([#] a) /\ ([#] B) is Element of bool the carrier of B
g is non empty TopSpace-like TopStruct
[#] g is non empty non proper open closed dense non boundary Element of bool the carrier of g
the carrier of g is non empty set
bool the carrier of g is non empty set
[: the carrier of g, the carrier of b:] is non empty Relation-like set
bool [: the carrier of g, the carrier of b:] is non empty set
g is non empty Relation-like the carrier of a -defined the carrier of b -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of b) Element of bool [: the carrier of a, the carrier of b:]
P is non empty Relation-like the carrier of B -defined the carrier of b -valued Function-like V17( the carrier of B) V21( the carrier of B, the carrier of b) Element of bool [: the carrier of B, the carrier of b:]

dom P is non empty Element of bool the carrier of B
dom g is non empty Element of bool the carrier of a
dom (g +* P) is set
rng (g +* P) is set
rng g is non empty Element of bool the carrier of b
bool the carrier of b is non empty set
rng P is non empty Element of bool the carrier of b
(rng g) \/ (rng P) is non empty Element of bool the carrier of b
c8 is non empty Relation-like the carrier of g -defined the carrier of b -valued Function-like V17( the carrier of g) V21( the carrier of g, the carrier of b) Element of bool [: the carrier of g, the carrier of b:]
s0 is Element of bool the carrier of b
c8 " s0 is Element of bool the carrier of g
g " s0 is Element of bool the carrier of a
P " s0 is Element of bool the carrier of B
dom c8 is non empty Element of bool the carrier of g
(dom g) \/ (dom P) is non empty set
HH is set
(c8 " s0) /\ ([#] B) is Element of bool the carrier of B
c8 . HH is set
P . HH is set
P . HH is set
c8 . HH is set
HH is set
c8 . HH is set
g . HH is set
P . HH is set
HH is set
(c8 " s0) /\ ([#] a) is Element of bool the carrier of a
c8 . HH is set
g . HH is set
g . HH is set
c8 . HH is set
s1 is Element of bool the carrier of a
AI is Element of bool the carrier of g
G9 is Element of bool the carrier of B
H is Element of bool the carrier of g
(c8 " s0) /\ (([#] a) \/ ([#] B)) is Element of bool the carrier of g
((c8 " s0) /\ ([#] a)) \/ ((c8 " s0) /\ ([#] B)) is set
(g " s0) \/ (P " s0) is set
a is TopStruct
id a is Relation-like the carrier of a -defined the carrier of a -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of a) Element of bool [: the carrier of a, the carrier of a:]
the carrier of a is set
[: the carrier of a, the carrier of a:] is Relation-like set
bool [: the carrier of a, the carrier of a:] is non empty set
id the carrier of a is Relation-like the carrier of a -defined the carrier of a -valued Function-like one-to-one V17( the carrier of a) V21( the carrier of a, the carrier of a) Element of bool [: the carrier of a, the carrier of a:]
bool the carrier of a is non empty set
b is Element of bool the carrier of a
(id a) .: b is Element of bool the carrier of a
bool the carrier of a is non empty set
b is Element of bool the carrier of a
(id a) " b is Element of bool the carrier of a
a is TopStruct
the carrier of a is set
[: the carrier of a, the carrier of a:] is Relation-like set
bool [: the carrier of a, the carrier of a:] is non empty set
id a is Relation-like the carrier of a -defined the carrier of a -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of a) continuous open Element of bool [: the carrier of a, the carrier of a:]
id the carrier of a is Relation-like the carrier of a -defined the carrier of a -valued Function-like one-to-one V17( the carrier of a) V21( the carrier of a, the carrier of a) Element of bool [: the carrier of a, the carrier of a:]
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
b is non empty TopSpace-like TopStruct
the carrier of b is non empty set
[: the carrier of a, the carrier of b:] is non empty Relation-like set
bool [: the carrier of a, the carrier of b:] is non empty set
B is non empty Relation-like the carrier of a -defined the carrier of b -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of b) Element of bool [: the carrier of a, the carrier of b:]
B /" is non empty Relation-like the carrier of b -defined the carrier of a -valued Function-like V17( the carrier of b) V21( the carrier of b, the carrier of a) Element of bool [: the carrier of b, the carrier of a:]
[: the carrier of b, the carrier of a:] is non empty Relation-like set
bool [: the carrier of b, the carrier of a:] is non empty set
rng B is non empty Element of bool the carrier of b
bool the carrier of b is non empty set
[#] b is non empty non proper open closed dense non boundary Element of bool the carrier of b
g is Element of bool the carrier of b
(B /") .: g is Element of bool the carrier of a
bool the carrier of a is non empty set
B " g is Element of bool the carrier of a
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
[: the carrier of I[01], the carrier of a:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of a:] is non empty set
b is Element of the carrier of a
I[01] --> b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) continuous Element of bool [: the carrier of I[01], the carrier of a:]
K324( the carrier of a, the carrier of I[01],b) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]
() . 0 is set
() . 1 is set
a is TopStruct
the carrier of a is set
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
g is Element of the carrier of a
[: the carrier of I[01], the carrier of a:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of a:] is non empty set
a is TopStruct
the carrier of a is set
b is Element of the carrier of a
B is Element of the carrier of a
[: the carrier of I[01], the carrier of a:] is Relation-like set
bool [: the carrier of I[01], the carrier of a:] is non empty set
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
b is Element of the carrier of a
I[01] --> b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) continuous Element of bool [: the carrier of I[01], the carrier of a:]
[: the carrier of I[01], the carrier of a:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of a:] is non empty set
K324( the carrier of a, the carrier of I[01],b) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]
() . 0 is set
() . 1 is set
is non empty trivial V33() V34() V35() connected compact Element of bool the carrier of I[01]
bool the carrier of I[01] is non empty set

the carrier of () is non empty V33() V34() V35() set
[: the carrier of I[01], the carrier of ():] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of ():] is non empty set
b is V31() real ext-real Element of the carrier of ()
I[01] --> b is non empty Relation-like the carrier of I[01] -defined the carrier of () -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of ()) continuous Element of bool [: the carrier of I[01], the carrier of ():]
K324( the carrier of (), the carrier of I[01],b) is non empty Relation-like the carrier of I[01] -defined the carrier of () -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of ()) Element of bool [: the carrier of I[01], the carrier of ():]
g is V31() real ext-real Element of the carrier of ()
g is V31() real ext-real Element of the carrier of ()
B is non empty Relation-like the carrier of I[01] -defined the carrier of () -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of ()) Element of bool [: the carrier of I[01], the carrier of ():]
B . 0 is set
B . 1 is set
a is () TopStruct
the carrier of a is set
[: the carrier of I[01], the carrier of a:] is Relation-like set
bool [: the carrier of I[01], the carrier of a:] is non empty set
b is Element of the carrier of a
B is Element of the carrier of a
g is Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]
g . 0 is set
g . 1 is set
g is Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]
g . 0 is set
g . 1 is set
a is () TopStruct
the carrier of a is set
b is Element of the carrier of a
B is Element of the carrier of a
g is Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V21( the carrier of I[01], the carrier of a) (a,b,B)
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
b is Element of the carrier of a
B is Element of the carrier of a
[: the carrier of I[01], the carrier of a:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of a:] is non empty set
g is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]
g . 0 is set
g . 1 is set
dom g is non empty V33() V34() V35() Element of bool the carrier of I[01]
rng g is non empty Element of bool the carrier of a
bool the carrier of a is non empty set
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
[: the carrier of I[01], the carrier of a:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of a:] is non empty set
b is Element of the carrier of a
B is Element of the carrier of a
g is Element of the carrier of a
g is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]
g . 0 is set
g . 1 is set
P is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]
P . 0 is set
P . 1 is set
rng g is non empty Element of bool the carrier of a
bool the carrier of a is non empty set
rng P is non empty Element of bool the carrier of a
(rng g) \/ (rng P) is non empty Element of bool the carrier of a
c8 is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,B)
c7 is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,B,g)
1 / 2 is V31() real ext-real Element of REAL
{ b1 where b1 is V31() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
Closed-Interval-TSpace (0,(1 / 2)) is non empty strict TopSpace-like V130() SubSpace of R^1
Closed-Interval-TSpace ((1 / 2),1) is non empty strict TopSpace-like V130() SubSpace of R^1
P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace ((1 / 2),1)) -defined the carrier of () -valued Function-like V17( the carrier of (Closed-Interval-TSpace ((1 / 2),1))) V21( the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of ()) Element of bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of ():]
the carrier of (Closed-Interval-TSpace ((1 / 2),1)) is non empty V33() V34() V35() set
[: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of ():] is non empty set
P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,(1 / 2))) -defined the carrier of () -valued Function-like V17( the carrier of (Closed-Interval-TSpace (0,(1 / 2)))) V21( the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of ()) Element of bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of ():]
the carrier of (Closed-Interval-TSpace (0,(1 / 2))) is non empty V33() V34() V35() set
[: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of ():] is non empty set
c8 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) is Relation-like the carrier of (Closed-Interval-TSpace (0,(1 / 2))) -defined the carrier of a -valued Function-like Element of bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of a:]
[: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of a:] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of a:] is non empty set
c7 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) is Relation-like the carrier of (Closed-Interval-TSpace ((1 / 2),1)) -defined the carrier of a -valued Function-like Element of bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of a:]
[: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of a:] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of a:] is non empty set
(c8 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (c7 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) is Relation-like Function-like set
dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace (0,(1 / 2)))
bool the carrier of (Closed-Interval-TSpace (0,(1 / 2))) is non empty set
[.0,(1 / 2).] is V33() V34() V35() V141() Element of bool REAL
dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace ((1 / 2),1))
bool the carrier of (Closed-Interval-TSpace ((1 / 2),1)) is non empty set
[.(1 / 2),1.] is V33() V34() V35() V141() Element of bool REAL
HH is TopSpace-like V130() SubSpace of I[01]
the carrier of HH is V33() V34() V35() set
[: the carrier of HH, the carrier of a:] is Relation-like set
bool [: the carrier of HH, the carrier of a:] is non empty set
HH is TopSpace-like V130() SubSpace of I[01]
the carrier of HH is V33() V34() V35() set
[: the carrier of HH, the carrier of a:] is Relation-like set
bool [: the carrier of HH, the carrier of a:] is non empty set
{ b1 where b1 is V31() real ext-real Element of REAL : ( 1 / 2 <= b1 & b1 <= 1 ) } is set
f is V31() real ext-real Element of REAL
(c7 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . f is set
2 * f is V31() real ext-real Element of REAL
(2 * f) - 1 is V31() real ext-real Element of REAL
c7 . ((2 * f) - 1) is set
t is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace ((1 / 2),1))
(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . t is V31() real ext-real Element of the carrier of ()
f is V31() real ext-real Element of REAL
f is V31() real ext-real Element of REAL
f - f is V31() real ext-real Element of REAL
1 - (1 / 2) is V31() real ext-real Element of REAL
(f - f) / (1 - (1 / 2)) is V31() real ext-real Element of REAL
((f - f) / (1 - (1 / 2))) * f is V31() real ext-real Element of REAL
1 * f is V31() real ext-real Element of REAL
(1 / 2) * f is V31() real ext-real Element of REAL
(1 * f) - ((1 / 2) * f) is V31() real ext-real Element of REAL
((1 * f) - ((1 / 2) * f)) / (1 - (1 / 2)) is V31() real ext-real Element of REAL
(((f - f) / (1 - (1 / 2))) * f) + (((1 * f) - ((1 / 2) * f)) / (1 - (1 / 2))) is V31() real ext-real Element of REAL
{ b1 where b1 is V31() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 / 2 ) } is set
f is V31() real ext-real Element of REAL
(c8 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . f is set
2 * f is V31() real ext-real Element of REAL
c8 . (2 * f) is set
t is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,(1 / 2)))
(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . t is V31() real ext-real Element of the carrier of ()
f is V31() real ext-real Element of REAL
f is V31() real ext-real Element of REAL
f - f is V31() real ext-real Element of REAL
(1 / 2) - 0 is V31() real ext-real Element of REAL
(f - f) / ((1 / 2) - 0) is V31() real ext-real Element of REAL
((f - f) / ((1 / 2) - 0)) * f is V31() real ext-real Element of REAL
(1 / 2) * f is V31() real ext-real Element of REAL
0 * f is V31() real ext-real Element of REAL
((1 / 2) * f) - (0 * f) is V31() real ext-real Element of REAL
(((1 / 2) * f) - (0 * f)) / ((1 / 2) - 0) is V31() real ext-real Element of REAL
(((f - f) / ((1 / 2) - 0)) * f) + ((((1 / 2) * f) - (0 * f)) / ((1 / 2) - 0)) is V31() real ext-real Element of REAL
ff is Relation-like the carrier of HH -defined the carrier of a -valued Function-like V17( the carrier of HH) V21( the carrier of HH, the carrier of a) Element of bool [: the carrier of HH, the carrier of a:]
ff . (1 / 2) is set
2 * (1 / 2) is V31() real ext-real Element of REAL
(2 * (1 / 2)) - 1 is V31() real ext-real Element of REAL
c7 . ((2 * (1 / 2)) - 1) is set
gg is Relation-like the carrier of HH -defined the carrier of a -valued Function-like V17( the carrier of HH) V21( the carrier of HH, the carrier of a) Element of bool [: the carrier of HH, the carrier of a:]
H is V31() real ext-real Element of the carrier of I[01]
gg . H is set
[#] HH is non proper V33() V34() V35() open closed dense Element of bool the carrier of HH
bool the carrier of HH is non empty set
[#] HH is non proper V33() V34() V35() open closed dense Element of bool the carrier of HH
bool the carrier of HH is non empty set
([#] HH) \/ ([#] HH) is V33() V34() V35() set
[#] I[01] is non empty non proper V33() V34() V35() open closed dense non boundary Element of bool the carrier of I[01]
([#] HH) /\ ([#] HH) is V33() V34() V35() Element of bool the carrier of HH
{H} is non empty trivial V33() V34() V35() connected compact Element of bool the carrier of I[01]
dom c8 is non empty V33() V34() V35() Element of bool the carrier of I[01]
rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of ()
bool the carrier of () is non empty set
dom c7 is non empty V33() V34() V35() Element of bool the carrier of I[01]
rng (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of ()
dom (c7 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) is V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace ((1 / 2),1))
{ b1 where b1 is V31() real ext-real Element of REAL : ( 1 / 2 <= b1 & b1 <= 1 ) } is set
f is V31() real ext-real Element of REAL
((c8 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (c7 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) . 0 is set
(c8 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . 0 is set
2 * 0 is V31() real ext-real Element of REAL
c8 . (2 * 0) is set
dom ((c8 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (c7 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) is set
dom (c8 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) is V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace (0,(1 / 2)))
(dom (c8 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (dom (c7 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) is V33() V34() V35() set
[.0,(1 / 2).] \/ [.(1 / 2),1.] is V33() V34() V35() Element of bool REAL
rng ((c8 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (c7 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) is set
rng (c8 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) is Element of bool the carrier of a
rng (c7 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) is Element of bool the carrier of a
(rng (c8 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (rng (c7 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) is Element of bool the carrier of a
f is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]
f is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) continuous Element of bool [: the carrier of I[01], the carrier of a:]
f . 1 is set
(c7 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . 1 is set
2 * 1 is V31() real ext-real Element of REAL
(2 * 1) - 1 is V31() real ext-real Element of REAL
c7 . ((2 * 1) - 1) is set
f is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,g)
t is V31() real ext-real Element of the carrier of I[01]
f . t is Element of the carrier of a
t9 is V31() real ext-real Element of REAL
2 * t9 is V31() real ext-real Element of REAL
c8 . (2 * t9) is set
(2 * t9) - 1 is V31() real ext-real Element of REAL
c7 . ((2 * t9) - 1) is set
{ b1 where b1 is V31() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 / 2 ) } is set
[.0,(1 / 2).] /\ [.(1 / 2),1.] is V33() V34() V35() V141() Element of bool REAL
{(1 / 2)} is non empty trivial V33() V34() V35() set
(c8 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t is set
(c7 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . (1 / 2) is set
(c7 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t is set
H is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,g)
H . 0 is set
H . 1 is set
H is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,g)
H . 0 is set
H . 1 is set
rng H is non empty Element of bool the carrier of a
rng c8 is non empty Element of bool the carrier of a
rng c7 is non empty Element of bool the carrier of a
(rng c8) \/ (rng c7) is non empty Element of bool the carrier of a
dom c7 is non empty V33() V34() V35() Element of bool the carrier of I[01]
HH is set
dom c8 is non empty V33() V34() V35() Element of bool the carrier of I[01]
dom H is non empty V33() V34() V35() Element of bool the carrier of I[01]
HH is set
H . HH is set
HH is V31() real ext-real Element of REAL
2 * HH is V31() real ext-real Element of REAL
2 * (1 / 2) is V31() real ext-real Element of REAL
c8 . (2 * HH) is set
2 * HH is V31() real ext-real Element of REAL
2 * 1 is V31() real ext-real Element of REAL
1 + 1 is V31() real ext-real Element of REAL
(2 * HH) - 1 is V31() real ext-real Element of REAL
2 * (1 / 2) is V31() real ext-real Element of REAL
0 + 1 is V31() real ext-real Element of REAL
c7 . ((2 * HH) - 1) is set
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
b is Element of the carrier of a
B is Element of the carrier of a
g is Element of the carrier of a
1 / 2 is V31() real ext-real Element of REAL
g is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,B)
P is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,B,g)
{ b1 where b1 is V31() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
Closed-Interval-TSpace (0,(1 / 2)) is non empty strict TopSpace-like V130() SubSpace of R^1
Closed-Interval-TSpace ((1 / 2),1) is non empty strict TopSpace-like V130() SubSpace of R^1
P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace ((1 / 2),1)) -defined the carrier of () -valued Function-like V17( the carrier of (Closed-Interval-TSpace ((1 / 2),1))) V21( the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of ()) Element of bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of ():]
the carrier of (Closed-Interval-TSpace ((1 / 2),1)) is non empty V33() V34() V35() set
[: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of ():] is non empty set
P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,(1 / 2))) -defined the carrier of () -valued Function-like V17( the carrier of (Closed-Interval-TSpace (0,(1 / 2)))) V21( the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of ()) Element of bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of ():]
the carrier of (Closed-Interval-TSpace (0,(1 / 2))) is non empty V33() V34() V35() set
[: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of ():] is non empty set
g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) is Relation-like the carrier of (Closed-Interval-TSpace (0,(1 / 2))) -defined the carrier of a -valued Function-like Element of bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of a:]
[: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of a:] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of a:] is non empty set
P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) is Relation-like the carrier of (Closed-Interval-TSpace ((1 / 2),1)) -defined the carrier of a -valued Function-like Element of bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of a:]
[: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of a:] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of a:] is non empty set
(g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) is Relation-like Function-like set
dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace (0,(1 / 2)))
bool the carrier of (Closed-Interval-TSpace (0,(1 / 2))) is non empty set
[.0,(1 / 2).] is V33() V34() V35() V141() Element of bool REAL
dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace ((1 / 2),1))
bool the carrier of (Closed-Interval-TSpace ((1 / 2),1)) is non empty set
[.(1 / 2),1.] is V33() V34() V35() V141() Element of bool REAL
{ b1 where b1 is V31() real ext-real Element of REAL : ( 1 / 2 <= b1 & b1 <= 1 ) } is set
a is V31() real ext-real Element of REAL
(P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . a is set
2 * a is V31() real ext-real Element of REAL
(2 * a) - 1 is V31() real ext-real Element of REAL
P . ((2 * a) - 1) is set
b is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace ((1 / 2),1))
(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . b is V31() real ext-real Element of the carrier of ()
HH is V31() real ext-real Element of REAL
HH is V31() real ext-real Element of REAL
HH - HH is V31() real ext-real Element of REAL
1 - (1 / 2) is V31() real ext-real Element of REAL
(HH - HH) / (1 - (1 / 2)) is V31() real ext-real Element of REAL
((HH - HH) / (1 - (1 / 2))) * a is V31() real ext-real Element of REAL
1 * HH is V31() real ext-real Element of REAL
(1 / 2) * HH is V31() real ext-real Element of REAL
(1 * HH) - ((1 / 2) * HH) is V31() real ext-real Element of REAL
((1 * HH) - ((1 / 2) * HH)) / (1 - (1 / 2)) is V31() real ext-real Element of REAL
(((HH - HH) / (1 - (1 / 2))) * a) + (((1 * HH) - ((1 / 2) * HH)) / (1 - (1 / 2))) is V31() real ext-real Element of REAL
s0 is TopSpace-like V130() SubSpace of I[01]
the carrier of s0 is V33() V34() V35() set
[: the carrier of s0, the carrier of a:] is Relation-like set
bool [: the carrier of s0, the carrier of a:] is non empty set
c8 is TopSpace-like V130() SubSpace of I[01]
the carrier of c8 is V33() V34() V35() set
[: the carrier of c8, the carrier of a:] is Relation-like set
bool [: the carrier of c8, the carrier of a:] is non empty set
rng ((g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) is set
rng (g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) is Element of bool the carrier of a
bool the carrier of a is non empty set
rng (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) is Element of bool the carrier of a
(rng (g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (rng (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) is Element of bool the carrier of a
{ b1 where b1 is V31() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 / 2 ) } is set
b is V31() real ext-real Element of REAL
(g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . b is set
2 * b is V31() real ext-real Element of REAL
g . (2 * b) is set
t is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,(1 / 2)))
(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . t is V31() real ext-real Element of the carrier of ()
b is V31() real ext-real Element of REAL
a is V31() real ext-real Element of REAL
b - a is V31() real ext-real Element of REAL
(1 / 2) - 0 is V31() real ext-real Element of REAL
(b - a) / ((1 / 2) - 0) is V31() real ext-real Element of REAL
((b - a) / ((1 / 2) - 0)) * b is V31() real ext-real Element of REAL
(1 / 2) * a is V31() real ext-real Element of REAL
0 * b is V31() real ext-real Element of REAL
((1 / 2) * a) - (0 * b) is V31() real ext-real Element of REAL
(((1 / 2) * a) - (0 * b)) / (1 / 2) is V31() real ext-real Element of REAL
(((b - a) / ((1 / 2) - 0)) * b) + ((((1 / 2) * a) - (0 * b)) / (1 / 2)) is V31() real ext-real Element of REAL
HH is Relation-like the carrier of c8 -defined the carrier of a -valued Function-like V17( the carrier of c8) V21( the carrier of c8, the carrier of a) Element of bool [: the carrier of c8, the carrier of a:]
HH . (1 / 2) is set
2 * (1 / 2) is V31() real ext-real Element of REAL
g . (2 * (1 / 2)) is set
(2 * (1 / 2)) - 1 is V31() real ext-real Element of REAL
P . ((2 * (1 / 2)) - 1) is set
HH is Relation-like the carrier of s0 -defined the carrier of a -valued Function-like V17( the carrier of s0) V21( the carrier of s0, the carrier of a) Element of bool [: the carrier of s0, the carrier of a:]
c7 is V31() real ext-real Element of the carrier of I[01]
HH . c7 is set
dom g is non empty V33() V34() V35() Element of bool the carrier of I[01]
rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of ()
bool the carrier of () is non empty set
dom P is non empty V33() V34() V35() Element of bool the carrier of I[01]
rng (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) is non empty V33() V34() V35() Element of bool the carrier of ()
dom (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) is V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace ((1 / 2),1))
{ b1 where b1 is V31() real ext-real Element of REAL : ( 1 / 2 <= b1 & b1 <= 1 ) } is set
a is V31() real ext-real Element of REAL
((g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) . 0 is set
(g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . 0 is set
2 * 0 is V31() real ext-real Element of REAL
g . (2 * 0) is set
dom ((g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) is set
dom (g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) is V33() V34() V35() Element of bool the carrier of (Closed-Interval-TSpace (0,(1 / 2)))
(dom (g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (dom (P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) is V33() V34() V35() set
[.0,(1 / 2).] \/ [.(1 / 2),1.] is V33() V34() V35() Element of bool REAL
[#] c8 is non proper V33() V34() V35() open closed dense Element of bool the carrier of c8
bool the carrier of c8 is non empty set
[#] s0 is non proper V33() V34() V35() open closed dense Element of bool the carrier of s0
bool the carrier of s0 is non empty set
([#] c8) \/ ([#] s0) is V33() V34() V35() set
[#] I[01] is non empty non proper V33() V34() V35() open closed dense non boundary Element of bool the carrier of I[01]
([#] c8) /\ ([#] s0) is V33() V34() V35() Element of bool the carrier of s0
{c7} is non empty trivial V33() V34() V35() connected compact Element of bool the carrier of I[01]
[: the carrier of I[01], the carrier of a:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of a:] is non empty set
a is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]
b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) continuous Element of bool [: the carrier of I[01], the carrier of a:]
b . 1 is set
(P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . 1 is set
2 * 1 is V31() real ext-real Element of REAL
(2 * 1) - 1 is V31() real ext-real Element of REAL
P . ((2 * 1) - 1) is set
b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,g)
t is V31() real ext-real Element of the carrier of I[01]
b . t is Element of the carrier of a
2 * t is V31() real ext-real Element of REAL
g . (2 * t) is set
(2 * t) - 1 is V31() real ext-real Element of REAL
P . ((2 * t) - 1) is set
{ b1 where b1 is V31() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 / 2 ) } is set
[.0,(1 / 2).] /\ [.(1 / 2),1.] is V33() V34() V35() V141() Element of bool REAL
{(1 / 2)} is non empty trivial V33() V34() V35() set
(g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t is set
(g * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t is set
(P * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t is set
c7 is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,g)
c8 is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,g)
dom c7 is non empty V33() V34() V35() Element of bool the carrier of I[01]
s0 is set
c7 . s0 is set
c8 . s0 is set
{ b1 where b1 is V31() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
G9 is V31() real ext-real Element of REAL
s1 is V31() real ext-real Element of the carrier of I[01]
c7 . s1 is Element of the carrier of a
2 * G9 is V31() real ext-real Element of REAL
g . (2 * G9) is set
c8 . s1 is Element of the carrier of a
s1 is V31() real ext-real Element of the carrier of I[01]
c7 . s1 is Element of the carrier of a
2 * G9 is V31() real ext-real Element of REAL
(2 * G9) - 1 is V31() real ext-real Element of REAL
P . ((2 * G9) - 1) is set
c8 . s1 is Element of the carrier of a
dom c8 is non empty V33() V34() V35() Element of bool the carrier of I[01]
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
b is Element of the carrier of a
I[01] --> b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) continuous Element of bool [: the carrier of I[01], the carrier of a:]
[: the carrier of I[01], the carrier of a:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of a:] is non empty set
K324( the carrier of a, the carrier of I[01],b) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]
() . 0 is set
() . 1 is set
g is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)
dom g is non empty V33() V34() V35() Element of bool the carrier of I[01]
g is set
P is set
g . g is set
g . P is set
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
b is Element of the carrier of a
I[01] --> b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) continuous Element of bool [: the carrier of I[01], the carrier of a:]
[: the carrier of I[01], the carrier of a:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of a:] is non empty set
K324( the carrier of a, the carrier of I[01],b) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]
B is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like constant V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)
dom B is non empty V33() V34() V35() Element of bool the carrier of I[01]
{ b1 where b1 is V31() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
g is set
B . g is set
() . g is set
B . 0 is set
dom () is non empty V33() V34() V35() Element of bool the carrier of I[01]
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
b is Element of the carrier of a
B is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like constant V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)
(a,b,b,b,B,B) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)
dom B is non empty V33() V34() V35() Element of bool the carrier of I[01]
g is set
B . g is set
(a,b,b,b,B,B) . g is set
{ b1 where b1 is V31() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
P is V31() real ext-real Element of REAL
(1 / 2) * 2 is V31() real ext-real Element of REAL
P * 2 is V31() real ext-real Element of REAL
2 * P is V31() real ext-real Element of REAL
B . (2 * P) is set
g is V31() real ext-real Element of the carrier of I[01]
B . g is Element of the carrier of a
(1 / 2) * 2 is V31() real ext-real Element of REAL
P * 2 is V31() real ext-real Element of REAL
1 + 0 is V31() real ext-real Element of REAL
2 * P is V31() real ext-real Element of REAL
(2 * P) - 1 is V31() real ext-real Element of REAL
1 * 2 is V31() real ext-real Element of REAL
2 - 1 is V31() real ext-real Element of REAL
B . ((2 * P) - 1) is set
g is V31() real ext-real Element of the carrier of I[01]
B . g is Element of the carrier of a
dom (a,b,b,b,B,B) is non empty V33() V34() V35() Element of bool the carrier of I[01]
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
b is Element of the carrier of a
B is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like constant V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)
(a,b,b,b,B,B) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
b is Element of the carrier of a
B is Element of the carrier of a
g is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,B)
L[01] (((0,1) (#)),((#) (0,1))) is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like V17( the carrier of ()) V21( the carrier of (), the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty set
[: the carrier of I[01], the carrier of a:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of a:] is non empty set
g * (L[01] (((0,1) (#)),((#) (0,1)))) is Relation-like the carrier of () -defined the carrier of a -valued Function-like Element of bool [: the carrier of (), the carrier of a:]
[: the carrier of (), the carrier of a:] is non empty Relation-like set
bool [: the carrier of (), the carrier of a:] is non empty set
P is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) Element of bool [: the carrier of I[01], the carrier of a:]
c7 is V31() real ext-real Element of the carrier of I[01]
P . c7 is Element of the carrier of a
1 - c7 is V31() real ext-real Element of REAL
g . (1 - c7) is set
dom (L[01] (((0,1) (#)),((#) (0,1)))) is non empty V33() V34() V35() Element of bool the carrier of ()
bool the carrier of () is non empty set
c8 is V31() real ext-real Element of the carrier of ()
(L[01] (((0,1) (#)),((#) (0,1)))) . c8 is V31() real ext-real Element of the carrier of ()
g . ((L[01] (((0,1) (#)),((#) (0,1)))) . c8) is set
0 - 1 is V31() real ext-real Element of REAL
(0 - 1) * c7 is V31() real ext-real Element of REAL
((0 - 1) * c7) + 1 is V31() real ext-real Element of REAL
g . (((0 - 1) * c7) + 1) is set
1 * c7 is V31() real ext-real Element of REAL
1 - (1 * c7) is V31() real ext-real Element of REAL
g . (1 - (1 * c7)) is set
{ b1 where b1 is V31() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
dom (L[01] (((0,1) (#)),((#) (0,1)))) is non empty V33() V34() V35() Element of bool the carrier of ()
bool the carrier of () is non empty set
(L[01] (((0,1) (#)),((#) (0,1)))) . 0 is set
(L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) is V31() real ext-real Element of the carrier of ()
P . 0 is set
g . 1 is set
(L[01] (((0,1) (#)),((#) (0,1)))) . 1 is set
(L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) is V31() real ext-real Element of the carrier of ()
P . 1 is set
g . 0 is set
c7 is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,B,b)
c8 is V31() real ext-real Element of the carrier of I[01]
c7 . c8 is Element of the carrier of a
1 - c8 is V31() real ext-real Element of REAL
g . (1 - c8) is set
g is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,B,b)
P is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,B,b)
c7 is set
g . c7 is set
P . c7 is set
c8 is V31() real ext-real Element of the carrier of I[01]
g . c8 is Element of the carrier of a
1 - c8 is V31() real ext-real Element of REAL
g . (1 - c8) is set
P . c8 is Element of the carrier of a
dom g is non empty V33() V34() V35() Element of bool the carrier of I[01]
dom P is non empty V33() V34() V35() Element of bool the carrier of I[01]
a is V31() real ext-real Element of REAL
1 - a is V31() real ext-real Element of REAL
1 - 1 is V31() real ext-real Element of REAL
1 - 0 is V31() real ext-real Element of REAL
a is V31() real ext-real Element of REAL
1 - a is V31() real ext-real Element of REAL
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
b is Element of the carrier of a
B is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like constant V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)
(a,b,b,B) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)
dom B is non empty V33() V34() V35() Element of bool the carrier of I[01]
g is set
B . g is set
(a,b,b,B) . g is set
g is V31() real ext-real Element of REAL
1 - g is V31() real ext-real Element of REAL
P is V31() real ext-real Element of the carrier of I[01]
B . P is Element of the carrier of a
dom (a,b,b,B) is non empty V33() V34() V35() Element of bool the carrier of I[01]
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
b is Element of the carrier of a
B is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like constant V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)
(a,b,b,B) is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of a) (a,b,b)
b is non empty TopSpace-like TopStruct
the carrier of b is non empty set
bool the carrier of b is non empty set
bool (bool the carrier of b) is non empty set
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
[: the carrier of a, the carrier of b:] is non empty Relation-like set
bool [: the carrier of a, the carrier of b:] is non empty set
B is Element of bool (bool the carrier of b)
union B is Element of bool the carrier of b
g is non empty Relation-like the carrier of a -defined the carrier of b -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of b) Element of bool [: the carrier of a, the carrier of b:]
g " () is Element of bool the carrier of a
bool the carrier of a is non empty set
g " B is Element of bool (bool the carrier of a)
bool (bool the carrier of a) is non empty set
union (g " B) is Element of bool the carrier of a
P is set
g . P is set
g is Element of bool the carrier of b
c7 is set
g " c7 is Element of bool the carrier of a
c8 is Element of bool the carrier of a
g is set
P is set
dom g is non empty Element of bool the carrier of a
c7 is Element of bool the carrier of a
c8 is Element of bool the carrier of b
g " c8 is Element of bool the carrier of a
g . g is set
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
b is non empty TopSpace-like TopStruct
the carrier of b is non empty set
[: the carrier of a, the carrier of b:] is non empty Relation-like set
bool [: the carrier of a, the carrier of b:] is non empty set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
g is non empty TopSpace-like TopStruct
the carrier of g is non empty set
[: the carrier of B, the carrier of g:] is non empty Relation-like set
bool [: the carrier of B, the carrier of g:] is non empty set
g is non empty Relation-like the carrier of a -defined the carrier of b -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of b) Element of bool [: the carrier of a, the carrier of b:]
P is non empty Relation-like the carrier of B -defined the carrier of g -valued Function-like V17( the carrier of B) V21( the carrier of B, the carrier of g) Element of bool [: the carrier of B, the carrier of g:]

[:a,B:] is non empty strict TopSpace-like TopStruct
the carrier of [:a,B:] is non empty set
[:b,g:] is non empty strict TopSpace-like TopStruct
the carrier of [:b,g:] is non empty set
[: the carrier of [:a,B:], the carrier of [:b,g:]:] is non empty Relation-like set
bool [: the carrier of [:a,B:], the carrier of [:b,g:]:] is non empty set
[:g,P:] is non empty Relation-like [: the carrier of a, the carrier of B:] -defined [: the carrier of b, the carrier of g:] -valued Function-like V17([: the carrier of a, the carrier of B:]) V21([: the carrier of a, the carrier of B:],[: the carrier of b, the carrier of g:]) Element of bool [:[: the carrier of a, the carrier of B:],[: the carrier of b, the carrier of g:]:]
[: the carrier of a, the carrier of B:] is non empty Relation-like set
[: the carrier of b, the carrier of g:] is non empty Relation-like set
[:[: the carrier of a, the carrier of B:],[: the carrier of b, the carrier of g:]:] is non empty Relation-like set
bool [:[: the carrier of a, the carrier of B:],[: the carrier of b, the carrier of g:]:] is non empty set
rng [:g,P:] is non empty Relation-like the carrier of b -defined the carrier of g -valued Element of bool [: the carrier of b, the carrier of g:]
bool [: the carrier of b, the carrier of g:] is non empty set
dom [:g,P:] is non empty Relation-like the carrier of a -defined the carrier of B -valued Element of bool [: the carrier of a, the carrier of B:]
bool [: the carrier of a, the carrier of B:] is non empty set
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
[: the carrier of a, the carrier of B:] is non empty Relation-like set
bool [: the carrier of a, the carrier of B:] is non empty set
b is non empty TopSpace-like TopStruct
the carrier of b is non empty set
g is non empty TopSpace-like TopStruct
the carrier of g is non empty set
[: the carrier of b, the carrier of g:] is non empty Relation-like set
bool [: the carrier of b, the carrier of g:] is non empty set
[:B,g:] is non empty strict TopSpace-like TopStruct
the carrier of [:B,g:] is non empty set
bool the carrier of [:B,g:] is non empty set
[:a,b:] is non empty strict TopSpace-like TopStruct
the carrier of [:a,b:] is non empty set
g is non empty Relation-like the carrier of a -defined the carrier of B -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of B) continuous Element of bool [: the carrier of a, the carrier of B:]
P is non empty Relation-like the carrier of b -defined the carrier of g -valued Function-like V17( the carrier of b) V21( the carrier of b, the carrier of g) continuous Element of bool [: the carrier of b, the carrier of g:]
(a,B,b,g,g,P) is non empty Relation-like the carrier of [:a,b:] -defined the carrier of [:B,g:] -valued Function-like V17( the carrier of [:a,b:]) V21( the carrier of [:a,b:], the carrier of [:B,g:]) Element of bool [: the carrier of [:a,b:], the carrier of [:B,g:]:]
[: the carrier of [:a,b:], the carrier of [:B,g:]:] is non empty Relation-like set
bool [: the carrier of [:a,b:], the carrier of [:B,g:]:] is non empty set
c8 is Element of bool the carrier of [:B,g:]
c7 is Element of bool the carrier of [:B,g:]
Base-Appr c7 is open Element of bool (bool the carrier of [:B,g:])
bool (bool the carrier of [:B,g:]) is non empty set
bool the carrier of B is non empty set
bool the carrier of g is non empty set
{ [:b1,b2:] where b1 is Element of bool the carrier of B, b2 is Element of bool the carrier of g : ( [:b1,b2:] c= c7 & b1 is open & b2 is open ) } is set
(a,B,b,g,g,P) " c8 is Element of bool the carrier of [:a,b:]
bool the carrier of [:a,b:] is non empty set
s0 is Element of bool the carrier of B
s1 is Element of bool the carrier of g
[:s0,s1:] is Relation-like Element of bool the carrier of [:B,g:]
[#] B is non empty non proper open closed dense non boundary Element of bool the carrier of B
g " s0 is Element of bool the carrier of a
bool the carrier of a is non empty set
[#] g is non empty non proper open closed dense non boundary Element of bool the carrier of g
P " s1 is Element of bool the carrier of b
bool the carrier of b is non empty set
[:(g " s0),(P " s1):] is Relation-like Element of bool the carrier of [:a,b:]
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
[: the carrier of a, the carrier of B:] is non empty Relation-like set
bool [: the carrier of a, the carrier of B:] is non empty set
b is non empty TopSpace-like TopStruct
the carrier of b is non empty set
g is non empty TopSpace-like TopStruct
the carrier of g is non empty set
[: the carrier of b, the carrier of g:] is non empty Relation-like set
bool [: the carrier of b, the carrier of g:] is non empty set
[:B,g:] is non empty strict TopSpace-like TopStruct
the carrier of [:B,g:] is non empty set
bool the carrier of [:B,g:] is non empty set
[:a,b:] is non empty strict TopSpace-like TopStruct
the carrier of [:a,b:] is non empty set
g is non empty Relation-like the carrier of a -defined the carrier of B -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of B) continuous Element of bool [: the carrier of a, the carrier of B:]
P is non empty Relation-like the carrier of b -defined the carrier of g -valued Function-like V17( the carrier of b) V21( the carrier of b, the carrier of g) continuous Element of bool [: the carrier of b, the carrier of g:]
(a,B,b,g,g,P) is non empty Relation-like the carrier of [:a,b:] -defined the carrier of [:B,g:] -valued Function-like V17( the carrier of [:a,b:]) V21( the carrier of [:a,b:], the carrier of [:B,g:]) Element of bool [: the carrier of [:a,b:], the carrier of [:B,g:]:]
[: the carrier of [:a,b:], the carrier of [:B,g:]:] is non empty Relation-like set
bool [: the carrier of [:a,b:], the carrier of [:B,g:]:] is non empty set
c7 is Element of bool the carrier of [:B,g:]
(a,B,b,g,g,P) " c7 is Element of bool the carrier of [:a,b:]
bool the carrier of [:a,b:] is non empty set
bool (bool the carrier of [:a,b:]) is non empty set
Base-Appr c7 is open Element of bool (bool the carrier of [:B,g:])
bool (bool the carrier of [:B,g:]) is non empty set
bool the carrier of B is non empty set
bool the carrier of g is non empty set
{ [:b1,b2:] where b1 is Element of bool the carrier of B, b2 is Element of bool the carrier of g : ( [:b1,b2:] c= c7 & b1 is open & b2 is open ) } is set
(a,B,b,g,g,P) " () is Element of bool (bool the carrier of [:a,b:])
c8 is Element of bool (bool the carrier of [:a,b:])
s0 is Element of bool the carrier of [:a,b:]
s1 is Element of bool the carrier of [:B,g:]
(a,B,b,g,g,P) " s1 is Element of bool the carrier of [:a,b:]
union () is Element of bool the carrier of [:B,g:]
union ((a,B,b,g,g,P) " ()) is Element of bool the carrier of [:a,b:]
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
[: the carrier of a, the carrier of B:] is non empty Relation-like set
bool [: the carrier of a, the carrier of B:] is non empty set
b is non empty TopSpace-like TopStruct
the carrier of b is non empty set
g is non empty TopSpace-like TopStruct
the carrier of g is non empty set
[: the carrier of b, the carrier of g:] is non empty Relation-like set
bool [: the carrier of b, the carrier of g:] is non empty set
[:a,b:] is non empty strict TopSpace-like TopStruct
the carrier of [:a,b:] is non empty set
[:B,g:] is non empty strict TopSpace-like TopStruct
the carrier of [:B,g:] is non empty set
[: the carrier of [:a,b:], the carrier of [:B,g:]:] is non empty Relation-like set
bool [: the carrier of [:a,b:], the carrier of [:B,g:]:] is non empty set
g is non empty Relation-like the carrier of a -defined the carrier of B -valued Function-like V17( the carrier of a) V21( the carrier of a, the carrier of B) continuous Element of bool [: the carrier of a, the carrier of B:]
P is non empty Relation-like the carrier of b -defined the carrier of g -valued Function-like V17( the carrier of b) V21( the carrier of b, the carrier of g) continuous Element of bool [: the carrier of b, the carrier of g:]
(a,B,b,g,g,P) is non empty Relation-like the carrier of [:a,b:] -defined the carrier of [:B,g:] -valued Function-like V17( the carrier of [:a,b:]) V21( the carrier of [:a,b:], the carrier of [:B,g:]) Element of bool [: the carrier of [:a,b:], the carrier of [:B,g:]:]
[#] [:B,g:] is non empty non proper open closed dense non boundary Element of bool the carrier of [:B,g:]
bool the carrier of [:B,g:] is non empty set
c7 is Element of bool the carrier of [:B,g:]
(a,B,b,g,g,P) " c7 is Element of bool the carrier of [:a,b:]
bool the carrier of [:a,b:] is non empty set
c7 is non empty Relation-like the carrier of [:a,b:] -defined the carrier of [:B,g:] -valued Function-like V17( the carrier of [:a,b:]) V21( the carrier of [:a,b:], the carrier of [:B,g:]) Element of bool [: the carrier of [:a,b:], the carrier of [:B,g:]:]

the carrier of [:a,b:] is set
g is Element of the carrier of [:a,b:]
g is Element of the carrier of [:a,b:]
the carrier of a is set
the carrier of b is set
[: the carrier of a, the carrier of b:] is Relation-like set
P is set
c7 is set
[P,c7] is non empty V18() set
{P,c7} is non empty set
{P} is non empty trivial set
{{P,c7},{P}} is non empty set
c8 is set
s0 is set
[c8,s0] is non empty V18() set
{c8,s0} is non empty set
{c8} is non empty trivial set
{{c8,s0},{c8}} is non empty set
AI is Element of the carrier of a
H is Element of the carrier of a
bool the carrier of a is non empty set
HH is Element of bool the carrier of a
[#] b is non proper open closed dense Element of bool the carrier of b
bool the carrier of b is non empty set
[:HH,([#] b):] is Relation-like Element of bool the carrier of [:a,b:]
bool the carrier of [:a,b:] is non empty set
AI is Element of the carrier of a
H is Element of the carrier of a
bool the carrier of b is non empty set
s1 is Element of the carrier of b
G9 is Element of the carrier of b
HH is Element of bool the carrier of b
[#] a is non proper open closed dense Element of bool the carrier of a
bool the carrier of a is non empty set
[:([#] a),HH:] is Relation-like Element of bool the carrier of [:a,b:]
bool the carrier of [:a,b:] is non empty set
AI is Element of the carrier of a
H is Element of the carrier of a
bool the carrier of [:a,b:] is non empty set
bool the carrier of [:a,b:] is non empty set