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
{} is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V138() V141() set
the empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V138() V141() set is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V138() V141() 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
I[01] is non empty strict TopSpace-like V130() TopStruct
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
[:[:1,1:],REAL:] is Relation-like set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is Relation-like set
[:[:REAL,REAL:],REAL:] is Relation-like set
bool [:[:REAL,REAL:],REAL:] 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
[:[:2,2:],REAL:] is 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
0 is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional natural V31() real V33() V34() V35() V36() V37() V38() V39() ext-real V138() V141() Element of NAT
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V130() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (0,1)) 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 (Closed-Interval-TSpace (0,1))
(0,1) (#) is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
TopSpaceMetr K300() is TopStruct
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
a is Relation-like Function-like 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:]
g +* P is Relation-like Function-like set
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:]
(I[01] --> b) . 0 is set
(I[01] --> b) . 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:]
(I[01] --> b) . 0 is set
(I[01] --> b) . 1 is set
{0[01]} 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
I[01] | {0[01]} is non empty strict TopSpace-like V130() SubSpace of I[01]
the carrier of (I[01] | {0[01]}) is non empty V33() V34() V35() set
[: the carrier of I[01], the carrier of (I[01] | {0[01]}):] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of (I[01] | {0[01]}):] is non empty set
b is V31() real ext-real Element of the carrier of (I[01] | {0[01]})
I[01] --> b is non empty Relation-like the carrier of I[01] -defined the carrier of (I[01] | {0[01]}) -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of (I[01] | {0[01]})) continuous Element of bool [: the carrier of I[01], the carrier of (I[01] | {0[01]}):]
K324( the carrier of (I[01] | {0[01]}), the carrier of I[01],b) is non empty Relation-like the carrier of I[01] -defined the carrier of (I[01] | {0[01]}) -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of (I[01] | {0[01]})) Element of bool [: the carrier of I[01], the carrier of (I[01] | {0[01]}):]
g is V31() real ext-real Element of the carrier of (I[01] | {0[01]})
g is V31() real ext-real Element of the carrier of (I[01] | {0[01]})
B is non empty Relation-like the carrier of I[01] -defined the carrier of (I[01] | {0[01]}) -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of (I[01] | {0[01]})) Element of bool [: the carrier of I[01], the carrier of (I[01] | {0[01]}):]
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 (Closed-Interval-TSpace (0,1)) -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 (Closed-Interval-TSpace (0,1))) Element of bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of (Closed-Interval-TSpace (0,1)):]
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 (Closed-Interval-TSpace (0,1)):] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of (Closed-Interval-TSpace (0,1)):] 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 (Closed-Interval-TSpace (0,1)) -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 (Closed-Interval-TSpace (0,1))) Element of bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of (Closed-Interval-TSpace (0,1)):]
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 (Closed-Interval-TSpace (0,1)):] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of (Closed-Interval-TSpace (0,1)):] 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 (Closed-Interval-TSpace (0,1))
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 (Closed-Interval-TSpace (0,1))
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 (Closed-Interval-TSpace (0,1))
bool the carrier of (Closed-Interval-TSpace (0,1)) 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 (Closed-Interval-TSpace (0,1))
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 (Closed-Interval-TSpace (0,1)) -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 (Closed-Interval-TSpace (0,1))) Element of bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of (Closed-Interval-TSpace (0,1)):]
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 (Closed-Interval-TSpace (0,1)):] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of (Closed-Interval-TSpace (0,1)):] 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 (Closed-Interval-TSpace (0,1)) -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 (Closed-Interval-TSpace (0,1))) Element of bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of (Closed-Interval-TSpace (0,1)):]
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 (Closed-Interval-TSpace (0,1)):] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of (Closed-Interval-TSpace (0,1)):] 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 (Closed-Interval-TSpace (0,1))
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 (Closed-Interval-TSpace (0,1))
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 (Closed-Interval-TSpace (0,1))
bool the carrier of (Closed-Interval-TSpace (0,1)) 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 (Closed-Interval-TSpace (0,1))
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:]
(I[01] --> b) . 0 is set
(I[01] --> b) . 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
(I[01] --> b) . g is set
B . 0 is set
dom (I[01] --> 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)
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 (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like V17( the carrier of (Closed-Interval-TSpace (0,1))) V21( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))) Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):]
[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):] 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 (Closed-Interval-TSpace (0,1)) -defined the carrier of a -valued Function-like Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of a:]
[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of a:] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (0,1)), 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 (Closed-Interval-TSpace (0,1))
bool the carrier of (Closed-Interval-TSpace (0,1)) is non empty set
c8 is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(L[01] (((0,1) (#)),((#) (0,1)))) . c8 is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
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 (Closed-Interval-TSpace (0,1))
bool the carrier of (Closed-Interval-TSpace (0,1)) 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 (Closed-Interval-TSpace (0,1))
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 (Closed-Interval-TSpace (0,1))
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 " (union B) 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:]
[:g,P:] is Relation-like Function-like 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,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) " (Base-Appr c7) 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 (Base-Appr c7) is Element of bool the carrier of [:B,g:]
union ((a,B,b,g,g,P) " (Base-Appr c7)) 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:]:]
a is TopSpace-like T_0 TopStruct
b is TopSpace-like T_0 TopStruct
[:a,b:] is strict TopSpace-like TopStruct
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
a is TopSpace-like T_0 T_1 TopStruct
b is TopSpace-like T_0 T_1 TopStruct