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
[:a,b:] is strict TopSpace-like T_0 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:]
bool the carrier of [:a,b:] is non empty set
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
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:]
[:HH,([#] b):] is Relation-like Element of bool the carrier of [:a,b:]
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
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
HH is Element of bool the carrier of b
[:([#] a),HH:] is Relation-like Element of bool the carrier of [:a,b:]
a is Element of bool the carrier of b
[:([#] a),a:] is Relation-like Element of bool the carrier of [:a,b:]
AI is Element of the carrier of a
H is Element of the carrier of a
a is TopSpace-like T_0 T_1 T_2 TopStruct
b is TopSpace-like T_0 T_1 T_2 TopStruct
[:a,b:] is strict TopSpace-like T_0 T_1 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:]
bool the carrier of [:a,b:] is non empty set
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
HH is Element of bool the carrier of a
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:]
a is Element of bool the carrier of a
[:a,([#] b):] is Relation-like Element of bool the carrier of [:a,b:]
b is Element of bool the carrier of [:a,b:]
b is Element of bool the carrier of [:a,b:]
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
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
HH is Element of bool the carrier of b
[:([#] a),HH:] is Relation-like Element of bool the carrier of [:a,b:]
a is Element of bool the carrier of b
[:([#] a),a:] is Relation-like Element of bool the carrier of [:a,b:]
b is Element of bool the carrier of [:a,b:]
b is Element of bool the carrier of [:a,b:]
AI is Element of the carrier of a
H is Element of the carrier of a
Closed-Interval-MSpace (0,1) is non empty V116() V121() V122() V123() V124() V126() SubSpace of K300()
TopSpaceMetr (Closed-Interval-MSpace (0,1)) is TopStruct
a is non empty 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
[:I[01],I[01]:] is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of [:I[01],I[01]:] is non empty set
[: the carrier of [:I[01],I[01]:], the carrier of a:] is non empty Relation-like set
bool [: the carrier of [:I[01],I[01]:], the carrier of a:] is non empty set
id the carrier of I[01] is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like one-to-one V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of I[01]) Element of bool [: the carrier of I[01], the carrier of I[01]:]
[: the carrier of I[01], the carrier of I[01]:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of I[01]:] is non empty set
id I[01] is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of I[01]) continuous open Element of bool [: the carrier of I[01], the carrier of I[01]:]
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
s0 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)
s1 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)
G9 is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like V17( the carrier of [:I[01],I[01]:]) V21( the carrier of [:I[01],I[01]:], the carrier of a) Element of bool [: the carrier of [:I[01],I[01]:], the carrier of a:]
P is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of I[01]) continuous Element of bool [: the carrier of I[01], the carrier of I[01]:]
c8 is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of I[01]) continuous Element of bool [: the carrier of I[01], the carrier of I[01]:]
(I[01],I[01],I[01],I[01],P,c8) is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:I[01],I[01]:] -valued Function-like V17( the carrier of [:I[01],I[01]:]) V21( the carrier of [:I[01],I[01]:], the carrier of [:I[01],I[01]:]) continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of [:I[01],I[01]:]:]
[: the carrier of [:I[01],I[01]:], the carrier of [:I[01],I[01]:]:] is non empty Relation-like set
bool [: the carrier of [:I[01],I[01]:], the carrier of [:I[01],I[01]:]:] is non empty set
G9 * (I[01],I[01],I[01],I[01],P,c8) is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like V17( the carrier of [:I[01],I[01]:]) V21( the carrier of [:I[01],I[01]:], the carrier of a) Element of bool [: the carrier of [:I[01],I[01]:], the carrier of a:]
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
H is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like V17( the carrier of [:I[01],I[01]:]) V21( the carrier of [:I[01],I[01]:], the carrier of a) Element of bool [: the carrier of [:I[01],I[01]:], the carrier of a:]
HH is V31() real ext-real Element of the carrier of I[01]
H . (HH,0) is set
[HH,0] is non empty V18() set
{HH,0} is non empty V33() V34() V35() set
{HH} is non empty trivial V33() V34() V35() set
{{HH,0},{HH}} is non empty set
H . [HH,0] is set
s1 . HH is Element of the carrier of a
H . (HH,1) is set
[HH,1] is non empty V18() set
{HH,1} is non empty V33() V34() V35() set
{{HH,1},{HH}} is non empty set
H . [HH,1] is set
s0 . HH is Element of the carrier of a
HH is V31() real ext-real Element of the carrier of I[01]
(L[01] (((0,1) (#)),((#) (0,1)))) . HH is set
HH is V31() real ext-real Element of REAL
1 - HH is V31() real ext-real Element of REAL
a is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(L[01] (((0,1) (#)),((#) (0,1)))) . a is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
0 - 1 is V31() real ext-real Element of REAL
(0 - 1) * HH is V31() real ext-real Element of REAL
((0 - 1) * HH) + 1 is V31() real ext-real Element of REAL
1 * HH is V31() real ext-real Element of REAL
1 - (1 * HH) is V31() real ext-real Element of REAL
dom (id the carrier of I[01]) is non empty V33() V34() V35() Element of bool the carrier of I[01]
dom (I[01],I[01],I[01],I[01],P,c8) is non empty Element of bool the carrier of [:I[01],I[01]:]
bool the carrier of [:I[01],I[01]:] is non empty set
[:(dom (id the carrier of I[01])),(dom (L[01] (((0,1) (#)),((#) (0,1))))):] is non empty Relation-like Element of bool the carrier of [:I[01],(Closed-Interval-TSpace (0,1)):]
[:I[01],(Closed-Interval-TSpace (0,1)):] is non empty strict TopSpace-like TopStruct
the carrier of [:I[01],(Closed-Interval-TSpace (0,1)):] is non empty set
bool the carrier of [:I[01],(Closed-Interval-TSpace (0,1)):] is non empty set
(I[01],I[01],I[01],I[01],P,c8) . (HH,1) is set
(I[01],I[01],I[01],I[01],P,c8) . [HH,1] is set
(id the carrier of I[01]) . HH is V31() real ext-real Element of the carrier of I[01]
(L[01] (((0,1) (#)),((#) (0,1)))) . 1 is set
[((id the carrier of I[01]) . HH),((L[01] (((0,1) (#)),((#) (0,1)))) . 1)] is non empty V18() set
{((id the carrier of I[01]) . HH),((L[01] (((0,1) (#)),((#) (0,1)))) . 1)} is non empty set
{((id the carrier of I[01]) . HH)} is non empty trivial V33() V34() V35() set
{{((id the carrier of I[01]) . HH),((L[01] (((0,1) (#)),((#) (0,1)))) . 1)},{((id the carrier of I[01]) . HH)}} is non empty set
(L[01] (((0,1) (#)),((#) (0,1)))) . 1[01] is set
[HH,((L[01] (((0,1) (#)),((#) (0,1)))) . 1[01])] is non empty V18() set
{HH,((L[01] (((0,1) (#)),((#) (0,1)))) . 1[01])} is non empty set
{{HH,((L[01] (((0,1) (#)),((#) (0,1)))) . 1[01])},{HH}} is non empty set
1 - 1 is V31() real ext-real Element of REAL
[HH,(1 - 1)] is non empty V18() set
{HH,(1 - 1)} is non empty V33() V34() V35() set
{{HH,(1 - 1)},{HH}} is non empty set
G9 . (HH,0) is set
G9 . [HH,0] is set
(I[01],I[01],I[01],I[01],P,c8) . (HH,0) is set
(I[01],I[01],I[01],I[01],P,c8) . [HH,0] is set
(L[01] (((0,1) (#)),((#) (0,1)))) . 0 is set
[((id the carrier of I[01]) . HH),((L[01] (((0,1) (#)),((#) (0,1)))) . 0)] is non empty V18() set
{((id the carrier of I[01]) . HH),((L[01] (((0,1) (#)),((#) (0,1)))) . 0)} is non empty set
{{((id the carrier of I[01]) . HH),((L[01] (((0,1) (#)),((#) (0,1)))) . 0)},{((id the carrier of I[01]) . HH)}} is non empty set
(L[01] (((0,1) (#)),((#) (0,1)))) . 0[01] is set
[HH,((L[01] (((0,1) (#)),((#) (0,1)))) . 0[01])] is non empty V18() set
{HH,((L[01] (((0,1) (#)),((#) (0,1)))) . 0[01])} is non empty set
{{HH,((L[01] (((0,1) (#)),((#) (0,1)))) . 0[01])},{HH}} is non empty set
1 - 0 is V31() real ext-real Element of REAL
[HH,(1 - 0)] is non empty V18() set
{HH,(1 - 0)} is non empty V33() V34() V35() set
{{HH,(1 - 0)},{HH}} is non empty set
G9 . (HH,1) is set
G9 . [HH,1] is set
HH is V31() real ext-real Element of the carrier of I[01]
H . (0,HH) is set
[0,HH] is non empty V18() set
{0,HH} is non empty V33() V34() V35() set
{0} is non empty trivial functional V33() V34() V35() V36() V37() V38() V136() V138() set
{{0,HH},{0}} is non empty set
H . [0,HH] is set
H . (1,HH) is set
[1,HH] is non empty V18() set
{1,HH} is non empty V33() V34() V35() set
{1} is non empty trivial V33() V34() V35() V36() V37() V38() V136() V138() set
{{1,HH},{1}} is non empty set
H . [1,HH] is set
HH is V31() real ext-real Element of the carrier of I[01]
(L[01] (((0,1) (#)),((#) (0,1)))) . HH is set
a is V31() real ext-real Element of REAL
1 - a is V31() real ext-real Element of REAL
b is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(L[01] (((0,1) (#)),((#) (0,1)))) . b is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
0 - 1 is V31() real ext-real Element of REAL
(0 - 1) * a is V31() real ext-real Element of REAL
((0 - 1) * a) + 1 is V31() real ext-real Element of REAL
1 * a is V31() real ext-real Element of REAL
1 - (1 * a) is V31() real ext-real Element of REAL
(L[01] (((0,1) (#)),((#) (0,1)))) . HH is set
HH is V31() real ext-real Element of REAL
1 - HH is V31() real ext-real Element of REAL
dom (id the carrier of I[01]) is non empty V33() V34() V35() Element of bool the carrier of I[01]
dom (I[01],I[01],I[01],I[01],P,c8) is non empty Element of bool the carrier of [:I[01],I[01]:]
bool the carrier of [:I[01],I[01]:] is non empty set
[:(dom (id the carrier of I[01])),(dom (L[01] (((0,1) (#)),((#) (0,1))))):] is non empty Relation-like Element of bool the carrier of [:I[01],(Closed-Interval-TSpace (0,1)):]
[:I[01],(Closed-Interval-TSpace (0,1)):] is non empty strict TopSpace-like TopStruct
the carrier of [:I[01],(Closed-Interval-TSpace (0,1)):] is non empty set
bool the carrier of [:I[01],(Closed-Interval-TSpace (0,1)):] is non empty set
(I[01],I[01],I[01],I[01],P,c8) . (1,HH) is set
(I[01],I[01],I[01],I[01],P,c8) . [1,HH] is set
(id the carrier of I[01]) . 1 is set
[((id the carrier of I[01]) . 1),((L[01] (((0,1) (#)),((#) (0,1)))) . HH)] is non empty V18() set
{((id the carrier of I[01]) . 1),((L[01] (((0,1) (#)),((#) (0,1)))) . HH)} is non empty set
{((id the carrier of I[01]) . 1)} is non empty trivial set
{{((id the carrier of I[01]) . 1),((L[01] (((0,1) (#)),((#) (0,1)))) . HH)},{((id the carrier of I[01]) . 1)}} is non empty set
[1,(1 - HH)] is non empty V18() set
{1,(1 - HH)} is non empty V33() V34() V35() set
{{1,(1 - HH)},{1}} is non empty set
HH is V31() real ext-real Element of the carrier of I[01]
G9 . (1,HH) is set
[1,HH] is non empty V18() set
{1,HH} is non empty V33() V34() V35() set
{{1,HH},{1}} is non empty set
G9 . [1,HH] is set
(I[01],I[01],I[01],I[01],P,c8) . (0,HH) is set
(I[01],I[01],I[01],I[01],P,c8) . [0,HH] is set
(id the carrier of I[01]) . 0 is set
[((id the carrier of I[01]) . 0),((L[01] (((0,1) (#)),((#) (0,1)))) . HH)] is non empty V18() set
{((id the carrier of I[01]) . 0),((L[01] (((0,1) (#)),((#) (0,1)))) . HH)} is non empty set
{((id the carrier of I[01]) . 0)} is non empty trivial set
{{((id the carrier of I[01]) . 0),((L[01] (((0,1) (#)),((#) (0,1)))) . HH)},{((id the carrier of I[01]) . 0)}} is non empty set
[0,(1 - HH)] is non empty V18() set
{0,(1 - HH)} is non empty V33() V34() V35() set
{{0,(1 - HH)},{0}} is non empty set
G9 . (0,HH) is set
[0,HH] is non empty V18() set
{0,HH} is non empty V33() V34() V35() set
{{0,HH},{0}} is non empty set
G9 . [0,HH] 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 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)
[: the carrier of I[01], the carrier of I[01]:] is non empty Relation-like set
g is set
g `1 is set
g . (g `1) is set
[:[: 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 I[01]:], the carrier of a:] is non empty set
g is non empty Relation-like [: the carrier of I[01], the carrier of I[01]:] -defined the carrier of a -valued Function-like V17([: the carrier of I[01], the carrier of I[01]:]) V21([: the carrier of I[01], the carrier of I[01]:], the carrier of a) Element of bool [:[: the carrier of I[01], the carrier of I[01]:], the carrier of a:]
[: the carrier of [:I[01],I[01]:], the carrier of a:] is non empty Relation-like set
bool [: the carrier of [:I[01],I[01]:], the carrier of a:] is non empty set
P is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like V17( the carrier of [:I[01],I[01]:]) V21( the carrier of [:I[01],I[01]:], the carrier of a) Element of bool [: the carrier of [:I[01],I[01]:], the carrier of a:]
c7 is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like V17( the carrier of [:I[01],I[01]:]) V21( the carrier of [:I[01],I[01]:], the carrier of a) Element of bool [: the carrier of [:I[01],I[01]:], the carrier of a:]
c8 is V31() real ext-real Element of the carrier of I[01]
c7 . (0,c8) is set
[0,c8] is non empty V18() set
{0,c8} is non empty V33() V34() V35() set
{0} is non empty trivial functional V33() V34() V35() V36() V37() V38() V136() V138() set
{{0,c8},{0}} is non empty set
c7 . [0,c8] is set
c7 . (1,c8) is set
[1,c8] is non empty V18() set
{1,c8} is non empty V33() V34() V35() set
{1} is non empty trivial V33() V34() V35() V36() V37() V38() V136() V138() set
{{1,c8},{1}} is non empty set
c7 . [1,c8] is set
[0,c8] `1 is set
g . ([0,c8] `1) is set
[1,c8] `1 is set
g . ([1,c8] `1) is set
g . 0 is set
g . 1 is set
c8 is Element of the carrier of [:I[01],I[01]:]
c7 . c8 is Element of the carrier of a
s0 is a_neighborhood of c7 . c8
c8 `1 is set
s1 is V31() real ext-real Element of the carrier of I[01]
g . s1 is Element of the carrier of a
AI is V33() V34() V35() Element of bool the carrier of I[01]
[#] I[01] is non empty non proper V33() V34() V35() open closed dense non boundary Element of bool the carrier of I[01]
Int AI is V33() V34() V35() open Element of bool the carrier of I[01]
c8 `2 is set
G9 is a_neighborhood of g . s1
H is V33() V34() V35() a_neighborhood of s1
g .: H is Element of bool the carrier of a
bool the carrier of a is non empty set
[:H, the carrier of I[01]:] is Relation-like set
bool the carrier of [:I[01],I[01]:] is non empty set
Int H is V33() V34() V35() open Element of bool the carrier of I[01]
HH is Element of bool the carrier of [:I[01],I[01]:]
Int HH is open Element of bool the carrier of [:I[01],I[01]:]
[:(Int H),(Int AI):] is Relation-like Element of bool the carrier of [:I[01],I[01]:]
HH is set
a is set
[HH,a] is non empty V18() set
{HH,a} is non empty set
{HH} is non empty trivial set
{{HH,a},{HH}} is non empty set
HH is a_neighborhood of c8
c7 .: HH is Element of bool the carrier of a
a is set
dom c7 is non empty Element of bool the carrier of [:I[01],I[01]:]
b is set
c7 . b is set
dom g is non empty V33() V34() V35() Element of bool the carrier of I[01]
b is Element of the carrier of [:I[01],I[01]:]
b `1 is set
c7 . b is Element of the carrier of a
g . (b `1) is set
c8 is V31() real ext-real Element of the carrier of I[01]
c7 . (c8,0) is set
[c8,0] is non empty V18() set
{c8,0} is non empty V33() V34() V35() set
{c8} is non empty trivial V33() V34() V35() set
{{c8,0},{c8}} is non empty set
c7 . [c8,0] is set
g . c8 is Element of the carrier of a
c7 . (c8,1) is set
[c8,1] is non empty V18() set
{c8,1} is non empty V33() V34() V35() set
{{c8,1},{c8}} is non empty set
c7 . [c8,1] is set
s1 is set
c7 . s1 is set
s1 `1 is set
g . (s1 `1) is set
s0 is set
c7 . s0 is set
s0 `1 is set
g . (s0 `1) is set
c8 is V31() real ext-real Element of the carrier of I[01]
c7 . (c8,0) is set
[c8,0] is non empty V18() set
{c8,0} is non empty V33() V34() V35() set
{c8} is non empty trivial V33() V34() V35() set
{{c8,0},{c8}} is non empty set
c7 . [c8,0] is set
g . c8 is Element of the carrier of a
s0 is V31() real ext-real Element of the carrier of I[01]
c7 . (s0,1) is set
[s0,1] is non empty V18() set
{s0,1} is non empty V33() V34() V35() set
{s0} is non empty trivial V33() V34() V35() set
{{s0,1},{s0}} is non empty set
c7 . [s0,1] is set
g . s0 is Element of the carrier of a
s1 is V31() real ext-real Element of the carrier of I[01]
c7 . (0,s1) is set
[0,s1] is non empty V18() set
{0,s1} is non empty V33() V34() V35() set
{0} is non empty trivial functional V33() V34() V35() V36() V37() V38() V136() V138() set
{{0,s1},{0}} is non empty set
c7 . [0,s1] is set
G9 is V31() real ext-real Element of the carrier of I[01]
c7 . (1,G9) is set
[1,G9] is non empty V18() set
{1,G9} is non empty V33() V34() V35() set
{1} is non empty trivial V33() V34() V35() V36() V37() V38() V136() V138() set
{{1,G9},{1}} is non empty set
c7 . [1,G9] is set
a is non empty TopSpace-like connected () 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
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) continuous (a,b,B)
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
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:]
b is Element of the carrier of a
g . 0 is set
B is Element of the carrier of a
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
g is Element of the carrier of a
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
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
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)
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) (a,B,g)
P . 0 is set
P . 1 is set
(a,b,B,g,g,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)
(a,b,B,g,g,P) . 0 is set
(a,b,B,g,g,P) . 1 is 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
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
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) Element of bool [: the carrier of I[01], the carrier of a:]
c7 . 0 is set
c7 . 1 is set
rng c7 is non empty Element of bool the carrier of a
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
bool the carrier of a is non empty set
the Element of the carrier of a is Element of the carrier of a
{ the Element of the carrier of a} is non empty trivial connected compact Element of bool the carrier of a
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
b is non empty TopSpace-like TopStruct
the carrier of b is non empty set
[: the carrier of I[01], the carrier of b:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of b:] is non empty set
B is Element of the carrier of b
g is Element of the carrier of b
g is non empty Relation-like the carrier of I[01] -defined the carrier of b -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of b) Element of bool [: the carrier of I[01], the carrier of b:]
g . 0 is set
g . 1 is set
g * (L[01] (((0,1) (#)),((#) (0,1)))) is Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of b -valued Function-like Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of b:]
[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of b:] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of b:] is non empty set
c7 is non empty Relation-like the carrier of I[01] -defined the carrier of b -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of b) Element of bool [: the carrier of I[01], the carrier of b:]
c7 . 0 is set
c7 . 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))
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))
a is V31() real ext-real Element of the carrier of I[01]
b is V31() real ext-real Element of the carrier of I[01]
[.a,b.] is V33() V34() V35() V141() Element of bool REAL
Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like V130() SubSpace of R^1
B is non empty V33() V34() V35() Element of bool the carrier of I[01]
I[01] | B is non empty strict TopSpace-like T_0 T_1 T_2 V130() SubSpace of I[01]
the carrier of (I[01] | B) is non empty V33() V34() V35() set
[: the carrier of I[01], the carrier of I[01]:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of I[01]:] is non empty set
(#) (a,b) is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (a,b))
the carrier of (Closed-Interval-TSpace (a,b)) is non empty V33() V34() V35() set
(a,b) (#) is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (a,b))
L[01] (((#) (a,b)),((a,b) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (a,b)) -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 (a,b))) Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (a,b)):]
[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (a,b)):] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (a,b)):] is non empty set
g is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of I[01]) Element of bool [: the carrier of I[01], the carrier of I[01]:]
g is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of I[01]) Element of bool [: the carrier of I[01], the carrier of I[01]:]
g . 0 is set
g . 1 is set
[.b,a.] is V33() V34() V35() V141() Element of bool REAL
Closed-Interval-TSpace (b,a) is non empty strict TopSpace-like V130() SubSpace of R^1
B is non empty V33() V34() V35() Element of bool the carrier of I[01]
I[01] | B is non empty strict TopSpace-like T_0 T_1 T_2 V130() SubSpace of I[01]
the carrier of (I[01] | B) is non empty V33() V34() V35() set
[: the carrier of I[01], the carrier of I[01]:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of I[01]:] is non empty set
(#) (b,a) is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (b,a))
the carrier of (Closed-Interval-TSpace (b,a)) is non empty V33() V34() V35() set
(b,a) (#) is V31() real ext-real Element of the carrier of (Closed-Interval-TSpace (b,a))
L[01] (((#) (b,a)),((b,a) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (b,a)) -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 (b,a))) Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,a)):]
[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,a)):] is non empty Relation-like set
bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,a)):] is non empty set
g is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of I[01]) Element of bool [: the carrier of I[01], the carrier of I[01]:]
g is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of I[01]) Element of bool [: the carrier of I[01], the carrier of I[01]:]
g . 0 is set
g . 1 is set
P is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of I[01]) ( I[01] ,b,a)
(I[01],b,a,P) is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of I[01]) ( I[01] ,a,b)
(I[01],b,a,P) . 0 is set
(I[01],b,a,P) . 1 is set
c7 is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of I[01]) Element of bool [: the carrier of I[01], the carrier of I[01]:]
c7 . 0 is set
c7 . 1 is set