REAL is non empty V45() V46() V47() V51() V52() set
NAT is V45() V46() V47() V48() V49() V50() V51() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V45() V51() V52() set
RAT is non empty V45() V46() V47() V48() V51() V52() set
INT is non empty V45() V46() V47() V48() V49() V51() V52() set
omega is V45() V46() V47() V48() V49() V50() V51() set
K6(omega) is set
K6(NAT) is set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(COMPLEX,REAL) is set
K6(K7(COMPLEX,REAL)) is set
I[01] is non empty strict TopSpace-like V146() TopStruct
the carrier of I[01] is non empty V45() V46() V47() set
1 is non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
K7(1,1) is set
K6(K7(1,1)) is set
K7(K7(1,1),1) is set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
K7(2,2) is set
K7(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is set
RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V146() MetrStruct
R^1 is non empty strict TopSpace-like V146() TopStruct
K7(K7(COMPLEX,COMPLEX),COMPLEX) is set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K6(K7(REAL,REAL)) is set
K7(RAT,RAT) is set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is set
K7(K7(NAT,NAT),NAT) is set
K6(K7(K7(NAT,NAT),NAT)) is set
{} is empty V45() V46() V47() V48() V49() V50() V51() set
0 is empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() Element of NAT
real_dist is V16() V19(K7(REAL,REAL)) V20( REAL ) Function-like V26(K7(REAL,REAL)) quasi_total Element of K6(K7(K7(REAL,REAL),REAL))
MetrStruct(# REAL,real_dist #) is strict MetrStruct
[.0,1.] is V45() V46() V47() Element of K6(REAL)
0[01] is V11() real ext-real Element of the carrier of I[01]
1[01] is V11() real ext-real Element of the carrier of I[01]
TopSpaceMetr RealSpace is TopStruct
the carrier of R^1 is non empty V45() V46() V47() set
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V146() SubSpace of R^1
K7( the carrier of R^1, the carrier of R^1) is set
K6(K7( the carrier of R^1, the carrier of R^1)) is set
f is set
X is V11() real ext-real set
Y is V11() real ext-real set
[.X,Y.] is V45() V46() V47() Element of K6(REAL)
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
f is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
[.X,Y.] is V45() V46() V47() Element of K6(REAL)
K6( the carrier of R^1) is set
X is V11() real ext-real set
Y is V11() real ext-real set
[.X,Y.] is V45() V46() V47() Element of K6(REAL)
f is V45() V46() V47() Element of K6( the carrier of R^1)
the carrier of (TopSpaceMetr RealSpace) is set
K6( the carrier of (TopSpaceMetr RealSpace)) is set
f ` is V45() V46() V47() Element of K6( the carrier of R^1)
the carrier of R^1 \ f is V45() V46() V47() set
the carrier of RealSpace is non empty V45() V46() V47() set
K6( the carrier of RealSpace) is set
a is Element of K6( the carrier of (TopSpaceMetr RealSpace))
B is V45() V46() V47() Element of K6( the carrier of RealSpace)
B ` is V45() V46() V47() Element of K6( the carrier of RealSpace)
the carrier of RealSpace \ B is V45() V46() V47() set
y is V11() real ext-real Element of the carrier of RealSpace
x is V11() real ext-real Element of REAL
b is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
[.b,g.] is V45() V46() V47() Element of K6(REAL)
{ b1 where b1 is V11() real ext-real Element of REAL : ( b <= b1 & b1 <= g ) } is set
b - x is V11() real ext-real Element of REAL
x is set
x is V11() real ext-real Element of REAL
Ball (y,x) is V45() V46() V47() Element of K6( the carrier of RealSpace)
{ b1 where b1 is V11() real ext-real Element of the carrier of RealSpace : not x <= dist (y,b1) } is set
H is V11() real ext-real Element of the carrier of RealSpace
H0 is V11() real ext-real Element of REAL
real_dist . (H0,x) is V11() real ext-real Element of REAL
H is V11() real ext-real Element of the carrier of RealSpace
dist (y,H) is V11() real ext-real Element of REAL
H0 - x is V11() real ext-real Element of REAL
abs (H0 - x) is V11() real ext-real Element of REAL
H is V11() real ext-real Element of REAL
x - g is V11() real ext-real Element of REAL
x is set
x is V11() real ext-real Element of REAL
Ball (y,x) is V45() V46() V47() Element of K6( the carrier of RealSpace)
{ b1 where b1 is V11() real ext-real Element of the carrier of RealSpace : not x <= dist (y,b1) } is set
H is V11() real ext-real Element of the carrier of RealSpace
H0 is V11() real ext-real Element of REAL
real_dist . (x,H0) is V11() real ext-real Element of REAL
H is V11() real ext-real Element of the carrier of RealSpace
dist (y,H) is V11() real ext-real Element of REAL
x - H0 is V11() real ext-real Element of REAL
abs (x - H0) is V11() real ext-real Element of REAL
H is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
Ball (y,x) is V45() V46() V47() Element of K6( the carrier of RealSpace)
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
[.X,Y.] is V45() V46() V47() Element of K6(REAL)
f is V45() V46() V47() Element of K6( the carrier of R^1)
X is V11() real ext-real set
Y is V11() real ext-real set
f is V11() real ext-real set
Closed-Interval-TSpace (Y,f) is non empty strict TopSpace-like V146() SubSpace of R^1
a is V11() real ext-real set
Closed-Interval-TSpace (X,a) is non empty strict TopSpace-like V146() SubSpace of R^1
[.Y,f.] is V45() V46() V47() Element of K6(REAL)
[.X,a.] is V45() V46() V47() Element of K6(REAL)
the carrier of (Closed-Interval-TSpace (Y,f)) is non empty V45() V46() V47() set
the carrier of (Closed-Interval-TSpace (X,a)) is non empty V45() V46() V47() set
X is V11() real ext-real set
Y is V11() real ext-real set
f is V11() real ext-real set
Closed-Interval-TSpace (X,f) is non empty strict TopSpace-like V146() SubSpace of R^1
Closed-Interval-TSpace (Y,f) is non empty strict TopSpace-like V146() SubSpace of R^1
a is V11() real ext-real set
Closed-Interval-TSpace (X,a) is non empty strict TopSpace-like V146() SubSpace of R^1
Closed-Interval-TSpace (Y,a) is non empty strict TopSpace-like V146() SubSpace of R^1
(Closed-Interval-TSpace (X,f)) union (Closed-Interval-TSpace (Y,a)) is non empty strict TopSpace-like V146() SubSpace of R^1
(Closed-Interval-TSpace (X,f)) meet (Closed-Interval-TSpace (Y,a)) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,f)) is non empty V45() V46() V47() set
[.X,f.] is V45() V46() V47() Element of K6(REAL)
the carrier of (Closed-Interval-TSpace (Y,a)) is non empty V45() V46() V47() set
[.Y,a.] is V45() V46() V47() Element of K6(REAL)
the carrier of (Closed-Interval-TSpace (X,a)) is non empty V45() V46() V47() set
[.X,a.] is V45() V46() V47() Element of K6(REAL)
the carrier of (Closed-Interval-TSpace (Y,f)) is non empty V45() V46() V47() set
[.Y,f.] is V45() V46() V47() Element of K6(REAL)
[.X,f.] \/ [.Y,a.] is V45() V46() V47() Element of K6(REAL)
[.X,f.] /\ [.Y,a.] is V45() V46() V47() Element of K6(REAL)
the carrier of (Closed-Interval-TSpace (X,f)) /\ the carrier of (Closed-Interval-TSpace (Y,a)) is V45() V46() V47() set
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
[.X,Y.] is V45() V46() V47() Element of K6(REAL)
[.X,Y.] is V45() V46() V47() Element of K6(REAL)
(0,1) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
the carrier of (Closed-Interval-TSpace (0,1)) is non empty V45() V46() V47() set
(0,1) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
X is V11() real ext-real set
Y is V11() real ext-real set
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
f is V11() real ext-real set
(X,f) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,f))
Closed-Interval-TSpace (X,f) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,f)) is non empty V45() V46() V47() set
(Y,f) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (Y,f))
Closed-Interval-TSpace (Y,f) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (Y,f)) is non empty V45() V46() V47() set
(X,f) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,f))
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
f is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
a is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
b is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
B is non empty V16() V19( REAL ) V20( REAL ) Function-like V26( REAL ) quasi_total Element of K6(K7(REAL,REAL))
[.X,Y.] is V45() V46() V47() Element of K6(REAL)
x is set
B | [.0,1.] is V16() V19( REAL ) V20( REAL ) Function-like Element of K6(K7(REAL,REAL))
rng (B | [.0,1.]) is V45() V46() V47() Element of K6(REAL)
B .: [.0,1.] is V45() V46() V47() Element of K6(REAL)
dom B is V45() V46() V47() Element of K6(REAL)
x is set
B . x is set
y is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
1 - x is V11() real ext-real Element of REAL
(1 - x) * b is V11() real ext-real Element of REAL
x * g is V11() real ext-real Element of REAL
((1 - x) * b) + (x * g) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( X <= b1 & b1 <= Y ) } is set
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
x * X is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
H0 is V11() real ext-real Element of REAL
x * Y is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
H0 is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
(1 - x) * Y is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
((1 - x) * Y) + (x * Y) is V11() real ext-real Element of REAL
(1 - x) * X is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
((1 - x) * X) + (x * X) is V11() real ext-real Element of REAL
dom (B | [.0,1.]) is V45() V46() V47() Element of K6(REAL)
(dom B) /\ [.0,1.] is V45() V46() V47() Element of K6(REAL)
REAL /\ [.0,1.] is V45() V46() V47() Element of K6(REAL)
x is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
y is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
x . y is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
1 - y is V11() real ext-real Element of REAL
(1 - y) * f is V11() real ext-real Element of REAL
y * a is V11() real ext-real set
((1 - y) * f) + (y * a) is V11() real ext-real Element of REAL
B . y is set
b is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
g is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
y is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
b . y is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
g . y is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
x is V11() real ext-real Element of REAL
1 - x is V11() real ext-real Element of REAL
B is V11() real ext-real Element of REAL
(1 - x) * B is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
x * x is V11() real ext-real Element of REAL
((1 - x) * B) + (x * x) is V11() real ext-real Element of REAL
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
f is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
a is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y,f,a) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
a - f is V11() real ext-real set
b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(X,Y,f,a) . b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(a - f) * b is V11() real ext-real set
((a - f) * b) + f is V11() real ext-real set
1 - b is V11() real ext-real Element of REAL
(1 - b) * f is V11() real ext-real Element of REAL
b * a is V11() real ext-real set
((1 - b) * f) + (b * a) is V11() real ext-real Element of REAL
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
f is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
a is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y,f,a) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
g is V11() real ext-real Element of REAL
b is V11() real ext-real Element of REAL
g - b is V11() real ext-real Element of REAL
B is non empty V16() V19( REAL ) V20( REAL ) Function-like V26( REAL ) quasi_total Element of K6(K7(REAL,REAL))
x is non empty V16() V19( the carrier of R^1) V20( the carrier of R^1) Function-like V26( the carrier of R^1) quasi_total Element of K6(K7( the carrier of R^1, the carrier of R^1))
y is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(X,Y,f,a) . y is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
x is V11() real ext-real Element of the carrier of R^1
x . x is V11() real ext-real Element of the carrier of R^1
x is V11() real ext-real Element of REAL
(g - b) * x is V11() real ext-real Element of REAL
((g - b) * x) + b is V11() real ext-real Element of REAL
y is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
K6( the carrier of (Closed-Interval-TSpace (X,Y))) is set
(X,Y,f,a) . y is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
K6( the carrier of (Closed-Interval-TSpace (0,1))) is set
x is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
[#] (Closed-Interval-TSpace (X,Y)) is non empty non proper V45() V46() V47() closed Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
x is V45() V46() V47() Element of K6( the carrier of R^1)
x /\ ([#] (Closed-Interval-TSpace (X,Y))) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
x is V11() real ext-real Element of the carrier of R^1
x . x is V11() real ext-real Element of the carrier of R^1
H0 is V45() V46() V47() Element of K6( the carrier of R^1)
x .: H0 is V45() V46() V47() Element of K6( the carrier of R^1)
[#] (Closed-Interval-TSpace (0,1)) is non empty non proper V45() V46() V47() closed Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
H0 /\ ([#] (Closed-Interval-TSpace (0,1))) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
H is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
H is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
(X,Y,f,a) .: H is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
t is set
dom (X,Y,f,a) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
r is set
(X,Y,f,a) . r is set
r is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(X,Y,f,a) .: the carrier of (Closed-Interval-TSpace (0,1)) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
p is V11() real ext-real Element of the carrier of R^1
[#] R^1 is non empty non proper V45() V46() V47() closed Element of K6( the carrier of R^1)
dom x is V45() V46() V47() Element of K6( the carrier of R^1)
x . p is V11() real ext-real Element of the carrier of R^1
H is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
(X,Y,f,a) .: H is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
f is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
a is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y,f,a) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
(X,Y,f,a) . (0,1) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y,f,a) . (0,1) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
1 - 0 is non empty V11() real ext-real positive non negative Element of REAL
b is V11() real ext-real Element of REAL
(1 - 0) * b is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
0 * g is V11() real ext-real Element of REAL
((1 - 0) * b) + (0 * g) is V11() real ext-real Element of REAL
1 - 1 is V11() real ext-real Element of REAL
(1 - 1) * b is V11() real ext-real Element of REAL
1 * g is V11() real ext-real Element of REAL
((1 - 1) * b) + (1 * g) is V11() real ext-real Element of REAL
(0,1,(0,1),(0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)))) is set
id (Closed-Interval-TSpace (0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))))
id the carrier of (Closed-Interval-TSpace (0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (0,1))) V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))))
X is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(0,1,(0,1),(0,1)) . X is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
Y is V11() real ext-real Element of REAL
1 - Y is V11() real ext-real Element of REAL
(1 - Y) * 0 is V11() real ext-real Element of REAL
Y * 1 is V11() real ext-real Element of REAL
((1 - Y) * 0) + (Y * 1) is V11() real ext-real Element of REAL
Y is V11() real ext-real set
X is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1)))) is set
f is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
a is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
Y - X is V11() real ext-real set
g is V11() real ext-real Element of REAL
B is V11() real ext-real Element of REAL
b is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
g - b is V11() real ext-real Element of REAL
y is non empty V16() V19( REAL ) V20( REAL ) Function-like V26( REAL ) quasi_total Element of K6(K7(REAL,REAL))
x is set
[.X,Y.] is V45() V46() V47() Element of K6(REAL)
y | [.X,Y.] is V16() V19( REAL ) V20( REAL ) Function-like Element of K6(K7(REAL,REAL))
rng (y | [.X,Y.]) is V45() V46() V47() Element of K6(REAL)
y .: [.X,Y.] is V45() V46() V47() Element of K6(REAL)
dom y is V45() V46() V47() Element of K6(REAL)
x is set
y . x is set
x is V11() real ext-real Element of REAL
H0 is V11() real ext-real Element of REAL
Y - H0 is V11() real ext-real Element of REAL
(Y - H0) * B is V11() real ext-real Element of REAL
H0 - X is V11() real ext-real Element of REAL
(H0 - X) * x is V11() real ext-real Element of REAL
((Y - H0) * B) + ((H0 - X) * x) is V11() real ext-real Element of REAL
(((Y - H0) * B) + ((H0 - X) * x)) / (Y - X) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
{ b1 where b1 is V11() real ext-real Element of REAL : ( X <= b1 & b1 <= Y ) } is set
H is V11() real ext-real Element of REAL
H is V11() real ext-real Element of REAL
H is V11() real ext-real Element of REAL
H is V11() real ext-real Element of REAL
- H0 is V11() real ext-real Element of REAL
Y + (- H0) is V11() real ext-real Element of REAL
(Y + (- H0)) + (H0 - X) is V11() real ext-real Element of REAL
(Y - X) / (Y - X) is V11() real ext-real Element of COMPLEX
H is V11() real ext-real Element of REAL
H is V11() real ext-real Element of REAL
dom (y | [.X,Y.]) is V45() V46() V47() Element of K6(REAL)
(dom y) /\ [.X,Y.] is V45() V46() V47() Element of K6(REAL)
REAL /\ [.X,Y.] is V45() V46() V47() Element of K6(REAL)
x is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
x is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
x . x is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
Y - x is V11() real ext-real set
(Y - x) * f is V11() real ext-real set
x - X is V11() real ext-real set
(x - X) * a is V11() real ext-real set
((Y - x) * f) + ((x - X) * a) is V11() real ext-real set
(((Y - x) * f) + ((x - X) * a)) / (Y - X) is V11() real ext-real Element of COMPLEX
y . x is set
b is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
g is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
B is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
b . B is set
g . B is set
b . B is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
x is V11() real ext-real Element of REAL
Y - x is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
(Y - x) * y is V11() real ext-real Element of REAL
x - X is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
(x - X) * x is V11() real ext-real Element of REAL
((Y - x) * y) + ((x - X) * x) is V11() real ext-real Element of REAL
(((Y - x) * y) + ((x - X) * x)) / (Y - X) is V11() real ext-real Element of REAL
g . B is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
Y - X is V11() real ext-real set
f is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
a is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(X,Y,f,a) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1)))) is set
a - f is V11() real ext-real set
(a - f) / (Y - X) is V11() real ext-real Element of COMPLEX
Y * f is V11() real ext-real set
X * a is V11() real ext-real set
(Y * f) - (X * a) is V11() real ext-real set
((Y * f) - (X * a)) / (Y - X) is V11() real ext-real Element of COMPLEX
b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y,f,a) . b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
((a - f) / (Y - X)) * b is V11() real ext-real set
(((a - f) / (Y - X)) * b) + (((Y * f) - (X * a)) / (Y - X)) is V11() real ext-real set
Y - b is V11() real ext-real set
(Y - b) * f is V11() real ext-real set
b - X is V11() real ext-real set
(b - X) * a is V11() real ext-real set
((Y - b) * f) + ((b - X) * a) is V11() real ext-real set
(((Y - b) * f) + ((b - X) * a)) / (Y - X) is V11() real ext-real Element of COMPLEX
b * (a - f) is V11() real ext-real set
(b * (a - f)) + ((Y * f) - (X * a)) is V11() real ext-real set
((b * (a - f)) + ((Y * f) - (X * a))) / (Y - X) is V11() real ext-real Element of COMPLEX
(b * (a - f)) / (Y - X) is V11() real ext-real Element of COMPLEX
((b * (a - f)) / (Y - X)) + (((Y * f) - (X * a)) / (Y - X)) is V11() real ext-real Element of COMPLEX
1 / (Y - X) is V11() real ext-real Element of REAL
(b * (a - f)) * (1 / (Y - X)) is V11() real ext-real Element of REAL
((b * (a - f)) * (1 / (Y - X))) + (((Y * f) - (X * a)) / (Y - X)) is V11() real ext-real Element of REAL
(a - f) * (1 / (Y - X)) is V11() real ext-real Element of REAL
((a - f) * (1 / (Y - X))) * b is V11() real ext-real Element of REAL
(((a - f) * (1 / (Y - X))) * b) + (((Y * f) - (X * a)) / (Y - X)) is V11() real ext-real Element of REAL
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
f is V11() real ext-real Element of REAL
a is V11() real ext-real Element of REAL
[.f,a.] is V45() V46() V47() Element of K6(REAL)
Closed-Interval-TSpace (f,a) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (f,a)) is non empty V45() V46() V47() set
b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(X,Y,b,g) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1)))) is set
x is V11() real ext-real Element of REAL
B is V11() real ext-real Element of REAL
x - B is V11() real ext-real Element of REAL
a - f is V11() real ext-real Element of REAL
(x - B) / (a - f) is V11() real ext-real Element of REAL
a * B is V11() real ext-real Element of REAL
f * x is V11() real ext-real Element of REAL
(a * B) - (f * x) is V11() real ext-real Element of REAL
((a * B) - (f * x)) / (a - f) is V11() real ext-real Element of REAL
y is non empty V16() V19( REAL ) V20( REAL ) Function-like V26( REAL ) quasi_total Element of K6(K7(REAL,REAL))
(f,a,b,g) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (f,a))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (f,a))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (f,a)), the carrier of (Closed-Interval-TSpace (0,1))))
K7( the carrier of (Closed-Interval-TSpace (f,a)), the carrier of (Closed-Interval-TSpace (0,1))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (f,a)), the carrier of (Closed-Interval-TSpace (0,1)))) is set
x is non empty V16() V19( the carrier of R^1) V20( the carrier of R^1) Function-like V26( the carrier of R^1) quasi_total Element of K6(K7( the carrier of R^1, the carrier of R^1))
x is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (f,a))
(f,a,b,g) . x is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
x is V11() real ext-real Element of the carrier of R^1
x . x is V11() real ext-real Element of the carrier of R^1
H0 is V11() real ext-real Element of REAL
((x - B) / (a - f)) * H0 is V11() real ext-real Element of REAL
(((x - B) / (a - f)) * H0) + (((a * B) - (f * x)) / (a - f)) is V11() real ext-real Element of REAL
x is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (f,a))
K6( the carrier of (Closed-Interval-TSpace (0,1))) is set
(f,a,b,g) . x is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
K6( the carrier of (Closed-Interval-TSpace (f,a))) is set
H0 is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
[#] (Closed-Interval-TSpace (0,1)) is non empty non proper V45() V46() V47() closed Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
H is V45() V46() V47() Element of K6( the carrier of R^1)
H /\ ([#] (Closed-Interval-TSpace (0,1))) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
x is V11() real ext-real Element of the carrier of R^1
x . x is V11() real ext-real Element of the carrier of R^1
H is V45() V46() V47() Element of K6( the carrier of R^1)
x .: H is V45() V46() V47() Element of K6( the carrier of R^1)
[#] (Closed-Interval-TSpace (f,a)) is non empty non proper V45() V46() V47() closed Element of K6( the carrier of (Closed-Interval-TSpace (f,a)))
H /\ ([#] (Closed-Interval-TSpace (f,a))) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (f,a)))
t is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (f,a)))
r is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (f,a)))
(f,a,b,g) .: r is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
r is set
dom (f,a,b,g) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (f,a)))
p is set
(f,a,b,g) . p is set
r0 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (f,a))
(f,a,b,g) .: the carrier of (Closed-Interval-TSpace (f,a)) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
W0 is V11() real ext-real Element of the carrier of R^1
[#] R^1 is non empty non proper V45() V46() V47() closed Element of K6( the carrier of R^1)
dom x is V45() V46() V47() Element of K6( the carrier of R^1)
x . W0 is V11() real ext-real Element of the carrier of R^1
t is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (f,a)))
(f,a,b,g) .: t is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
Y - X is V11() real ext-real set
f is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
a is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(X,Y,f,a) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1)))) is set
(X,Y,f,a) . (X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(X,Y,f,a) . (X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
b is V11() real ext-real Element of REAL
(Y - X) * b is V11() real ext-real Element of REAL
X - X is V11() real ext-real set
g is V11() real ext-real Element of REAL
(X - X) * g is V11() real ext-real Element of REAL
((Y - X) * b) + ((X - X) * g) is V11() real ext-real Element of REAL
(((Y - X) * b) + ((X - X) * g)) / (Y - X) is V11() real ext-real Element of REAL
Y - Y is V11() real ext-real set
(Y - Y) * b is V11() real ext-real Element of REAL
(Y - X) * g is V11() real ext-real Element of REAL
((Y - Y) * b) + ((Y - X) * g) is V11() real ext-real Element of REAL
(((Y - Y) * b) + ((Y - X) * g)) / (Y - X) is V11() real ext-real Element of REAL
(0,1,(0,1),(0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))))
X is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(0,1,(0,1),(0,1)) . X is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
Y is V11() real ext-real Element of REAL
1 - Y is V11() real ext-real Element of REAL
(1 - Y) * 0 is V11() real ext-real Element of REAL
Y - 0 is V11() real ext-real Element of REAL
(Y - 0) * 1 is V11() real ext-real Element of REAL
((1 - Y) * 0) + ((Y - 0) * 1) is V11() real ext-real Element of REAL
1 - 0 is non empty V11() real ext-real positive non negative Element of REAL
(((1 - Y) * 0) + ((Y - 0) * 1)) / (1 - 0) is V11() real ext-real Element of REAL
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
id (Closed-Interval-TSpace (X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
id the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
(X,Y,(0,1),(0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1)))) is set
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y,(X,Y),(X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
(X,Y,(X,Y),(X,Y)) * (X,Y,(0,1),(0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
(X,Y,(0,1),(0,1)) * (X,Y,(X,Y),(X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))))
Y - X is V11() real ext-real set
b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
((X,Y,(X,Y),(X,Y)) * (X,Y,(0,1),(0,1))) . b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y,(0,1),(0,1)) . b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
g is V11() real ext-real Element of REAL
Y - g is V11() real ext-real Element of REAL
(Y - g) * 0 is V11() real ext-real Element of REAL
g - X is V11() real ext-real Element of REAL
(g - X) * 1 is V11() real ext-real Element of REAL
((Y - g) * 0) + ((g - X) * 1) is V11() real ext-real Element of REAL
(((Y - g) * 0) + ((g - X) * 1)) / (Y - X) is V11() real ext-real Element of REAL
(g - X) / (Y - X) is V11() real ext-real Element of REAL
(X,Y,(X,Y),(X,Y)) . ((X,Y,(0,1),(0,1)) . b) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
1 - ((g - X) / (Y - X)) is V11() real ext-real Element of REAL
(1 - ((g - X) / (Y - X))) * X is V11() real ext-real Element of REAL
((g - X) / (Y - X)) * Y is V11() real ext-real Element of REAL
((1 - ((g - X) / (Y - X))) * X) + (((g - X) / (Y - X)) * Y) is V11() real ext-real Element of REAL
1 * (Y - X) is V11() real ext-real Element of REAL
(1 * (Y - X)) - (g - X) is V11() real ext-real Element of REAL
((1 * (Y - X)) - (g - X)) / (Y - X) is V11() real ext-real Element of REAL
(((1 * (Y - X)) - (g - X)) / (Y - X)) * X is V11() real ext-real Element of REAL
((((1 * (Y - X)) - (g - X)) / (Y - X)) * X) + (((g - X) / (Y - X)) * Y) is V11() real ext-real Element of REAL
(Y - g) / (Y - X) is V11() real ext-real Element of REAL
X / 1 is V11() real ext-real Element of REAL
((Y - g) / (Y - X)) * (X / 1) is V11() real ext-real Element of REAL
(((Y - g) / (Y - X)) * (X / 1)) + (((g - X) / (Y - X)) * Y) is V11() real ext-real Element of REAL
(Y - g) * X is V11() real ext-real Element of REAL
((Y - g) * X) / (1 * (Y - X)) is V11() real ext-real Element of REAL
(((Y - g) * X) / (1 * (Y - X))) + (((g - X) / (Y - X)) * Y) is V11() real ext-real Element of REAL
((Y - g) * X) / (Y - X) is V11() real ext-real Element of REAL
Y / 1 is V11() real ext-real Element of REAL
((g - X) / (Y - X)) * (Y / 1) is V11() real ext-real Element of REAL
(((Y - g) * X) / (Y - X)) + (((g - X) / (Y - X)) * (Y / 1)) is V11() real ext-real Element of REAL
(g - X) * Y is V11() real ext-real Element of REAL
((g - X) * Y) / (1 * (Y - X)) is V11() real ext-real Element of REAL
(((Y - g) * X) / (Y - X)) + (((g - X) * Y) / (1 * (Y - X))) is V11() real ext-real Element of REAL
X * Y is V11() real ext-real set
X * g is V11() real ext-real Element of REAL
(X * Y) - (X * g) is V11() real ext-real Element of REAL
((X * Y) - (X * g)) + ((g - X) * Y) is V11() real ext-real Element of REAL
(((X * Y) - (X * g)) + ((g - X) * Y)) / (Y - X) is V11() real ext-real Element of REAL
(Y - X) * g is V11() real ext-real Element of REAL
((Y - X) * g) / (Y - X) is V11() real ext-real Element of REAL
b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
((X,Y,(0,1),(0,1)) * (X,Y,(X,Y),(X,Y))) . b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(X,Y,(X,Y),(X,Y)) . b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
g is V11() real ext-real Element of REAL
1 - g is V11() real ext-real Element of REAL
(1 - g) * X is V11() real ext-real Element of REAL
g * Y is V11() real ext-real Element of REAL
((1 - g) * X) + (g * Y) is V11() real ext-real Element of REAL
g * (Y - X) is V11() real ext-real Element of REAL
(g * (Y - X)) + X is V11() real ext-real Element of REAL
(X,Y,(0,1),(0,1)) . ((X,Y,(X,Y),(X,Y)) . b) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
Y - ((g * (Y - X)) + X) is V11() real ext-real Element of REAL
(Y - ((g * (Y - X)) + X)) * 0 is V11() real ext-real Element of REAL
((g * (Y - X)) + X) - X is V11() real ext-real Element of REAL
(((g * (Y - X)) + X) - X) * 1 is V11() real ext-real Element of REAL
((Y - ((g * (Y - X)) + X)) * 0) + ((((g * (Y - X)) + X) - X) * 1) is V11() real ext-real Element of REAL
(((Y - ((g * (Y - X)) + X)) * 0) + ((((g * (Y - X)) + X) - X) * 1)) / (Y - X) is V11() real ext-real Element of REAL
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
id (Closed-Interval-TSpace (X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
id the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
(X,Y,(0,1),(0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1)))) is set
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y,(X,Y),(X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
(X,Y,(X,Y),(X,Y)) * (X,Y,(0,1),(0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
(X,Y,(0,1),(0,1)) * (X,Y,(X,Y),(X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))))
Y - X is V11() real ext-real set
b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
((X,Y,(X,Y),(X,Y)) * (X,Y,(0,1),(0,1))) . b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y,(0,1),(0,1)) . b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
g is V11() real ext-real Element of REAL
Y - g is V11() real ext-real Element of REAL
(Y - g) * 1 is V11() real ext-real Element of REAL
g - X is V11() real ext-real Element of REAL
(g - X) * 0 is V11() real ext-real Element of REAL
((Y - g) * 1) + ((g - X) * 0) is V11() real ext-real Element of REAL
(((Y - g) * 1) + ((g - X) * 0)) / (Y - X) is V11() real ext-real Element of REAL
(Y - g) / (Y - X) is V11() real ext-real Element of REAL
(X,Y,(X,Y),(X,Y)) . ((X,Y,(0,1),(0,1)) . b) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
1 - ((Y - g) / (Y - X)) is V11() real ext-real Element of REAL
(1 - ((Y - g) / (Y - X))) * Y is V11() real ext-real Element of REAL
((Y - g) / (Y - X)) * X is V11() real ext-real Element of REAL
((1 - ((Y - g) / (Y - X))) * Y) + (((Y - g) / (Y - X)) * X) is V11() real ext-real Element of REAL
1 * (Y - X) is V11() real ext-real Element of REAL
(1 * (Y - X)) - (Y - g) is V11() real ext-real Element of REAL
((1 * (Y - X)) - (Y - g)) / (Y - X) is V11() real ext-real Element of REAL
(((1 * (Y - X)) - (Y - g)) / (Y - X)) * Y is V11() real ext-real Element of REAL
((((1 * (Y - X)) - (Y - g)) / (Y - X)) * Y) + (((Y - g) / (Y - X)) * X) is V11() real ext-real Element of REAL
(g - X) / (Y - X) is V11() real ext-real Element of REAL
Y / 1 is V11() real ext-real Element of REAL
((g - X) / (Y - X)) * (Y / 1) is V11() real ext-real Element of REAL
(((g - X) / (Y - X)) * (Y / 1)) + (((Y - g) / (Y - X)) * X) is V11() real ext-real Element of REAL
(g - X) * Y is V11() real ext-real Element of REAL
((g - X) * Y) / (1 * (Y - X)) is V11() real ext-real Element of REAL
(((g - X) * Y) / (1 * (Y - X))) + (((Y - g) / (Y - X)) * X) is V11() real ext-real Element of REAL
((g - X) * Y) / (Y - X) is V11() real ext-real Element of REAL
X / 1 is V11() real ext-real Element of REAL
((Y - g) / (Y - X)) * (X / 1) is V11() real ext-real Element of REAL
(((g - X) * Y) / (Y - X)) + (((Y - g) / (Y - X)) * (X / 1)) is V11() real ext-real Element of REAL
(Y - g) * X is V11() real ext-real Element of REAL
((Y - g) * X) / (1 * (Y - X)) is V11() real ext-real Element of REAL
(((g - X) * Y) / (Y - X)) + (((Y - g) * X) / (1 * (Y - X))) is V11() real ext-real Element of REAL
Y * g is V11() real ext-real Element of REAL
Y * X is V11() real ext-real set
(Y * g) - (Y * X) is V11() real ext-real Element of REAL
((Y * g) - (Y * X)) + ((Y - g) * X) is V11() real ext-real Element of REAL
(((Y * g) - (Y * X)) + ((Y - g) * X)) / (Y - X) is V11() real ext-real Element of REAL
(Y - X) * g is V11() real ext-real Element of REAL
((Y - X) * g) / (Y - X) is V11() real ext-real Element of REAL
b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
((X,Y,(0,1),(0,1)) * (X,Y,(X,Y),(X,Y))) . b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(X,Y,(X,Y),(X,Y)) . b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
g is V11() real ext-real Element of REAL
1 - g is V11() real ext-real Element of REAL
(1 - g) * Y is V11() real ext-real Element of REAL
g * X is V11() real ext-real Element of REAL
((1 - g) * Y) + (g * X) is V11() real ext-real Element of REAL
X - Y is V11() real ext-real set
g * (X - Y) is V11() real ext-real Element of REAL
(g * (X - Y)) + Y is V11() real ext-real Element of REAL
(X,Y,(0,1),(0,1)) . ((X,Y,(X,Y),(X,Y)) . b) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
Y - ((g * (X - Y)) + Y) is V11() real ext-real Element of REAL
(Y - ((g * (X - Y)) + Y)) * 1 is V11() real ext-real Element of REAL
((g * (X - Y)) + Y) - X is V11() real ext-real Element of REAL
(((g * (X - Y)) + Y) - X) * 0 is V11() real ext-real Element of REAL
((Y - ((g * (X - Y)) + Y)) * 1) + ((((g * (X - Y)) + Y) - X) * 0) is V11() real ext-real Element of REAL
(((Y - ((g * (X - Y)) + Y)) * 1) + ((((g * (X - Y)) + Y) - X) * 0)) / (Y - X) is V11() real ext-real Element of REAL
- (X - Y) is V11() real ext-real set
g * (- (X - Y)) is V11() real ext-real Element of REAL
(g * (- (X - Y))) / (Y - X) is V11() real ext-real Element of REAL
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y,(X,Y),(X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
(X,Y,(X,Y),(X,Y)) /" is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1)))) is set
(X,Y,(0,1),(0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
(X,Y,(0,1),(0,1)) /" is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
(X,Y,(0,1),(0,1)) * (X,Y,(X,Y),(X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))))
id the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
id (Closed-Interval-TSpace (X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
(X,Y,(X,Y),(X,Y)) * (X,Y,(0,1),(0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
rng (X,Y,(X,Y),(X,Y)) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
K6( the carrier of (Closed-Interval-TSpace (X,Y))) is set
[#] (Closed-Interval-TSpace (X,Y)) is non empty non proper V45() V46() V47() closed Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
(X,Y,(X,Y),(X,Y)) " is V16() Function-like set
dom (X,Y,(X,Y),(X,Y)) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
K6( the carrier of (Closed-Interval-TSpace (0,1))) is set
[#] (Closed-Interval-TSpace (0,1)) is non empty non proper V45() V46() V47() closed Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
rng (X,Y,(0,1),(0,1)) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
(X,Y,(0,1),(0,1)) " is V16() Function-like set
dom (X,Y,(0,1),(0,1)) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y,(X,Y),(X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
(X,Y,(X,Y),(X,Y)) /" is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1)))) is set
(X,Y,(0,1),(0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
(X,Y,(0,1),(0,1)) /" is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
(X,Y,(0,1),(0,1)) * (X,Y,(X,Y),(X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))))
id the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
id (Closed-Interval-TSpace (X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
(X,Y,(X,Y),(X,Y)) * (X,Y,(0,1),(0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
rng (X,Y,(X,Y),(X,Y)) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
K6( the carrier of (Closed-Interval-TSpace (X,Y))) is set
[#] (Closed-Interval-TSpace (X,Y)) is non empty non proper V45() V46() V47() closed Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
(X,Y,(X,Y),(X,Y)) " is V16() Function-like set
dom (X,Y,(X,Y),(X,Y)) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
K6( the carrier of (Closed-Interval-TSpace (0,1))) is set
[#] (Closed-Interval-TSpace (0,1)) is non empty non proper V45() V46() V47() closed Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
rng (X,Y,(0,1),(0,1)) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
(X,Y,(0,1),(0,1)) " is V16() Function-like set
dom (X,Y,(0,1),(0,1)) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
K6( the carrier of I[01]) is set
[#] I[01] is non empty non proper V45() V46() V47() closed Element of K6( the carrier of I[01])
{} I[01] is empty V45() V46() V47() V48() V49() V50() V51() closed connected Element of K6( the carrier of I[01])
X is V45() V46() V47() Element of K6( the carrier of I[01])
Y is V45() V46() V47() Element of K6( the carrier of I[01])
X \/ Y is V45() V46() V47() Element of K6( the carrier of I[01])
f is V45() V46() V47() Element of K6(REAL)
the V11() real ext-real Element of f is V11() real ext-real Element of f
g is V11() real ext-real Element of REAL
B is V11() real ext-real Element of REAL
a is V45() V46() V47() Element of K6(REAL)
the V11() real ext-real Element of a is V11() real ext-real Element of a
x is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
the carrier of RealSpace is non empty V45() V46() V47() set
the carrier of (TopSpaceMetr RealSpace) is set
y is ext-real set
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
x is V11() real ext-real Element of REAL
y is ext-real set
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
x is V11() real ext-real Element of REAL
y is V45() V46() V47() Element of K6( the carrier of R^1)
x is V45() V46() V47() Element of K6( the carrier of R^1)
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
x ` is V45() V46() V47() Element of K6( the carrier of R^1)
the carrier of R^1 \ x is V45() V46() V47() set
lower_bound a is V11() real ext-real Element of REAL
H0 is V11() real ext-real Element of the carrier of RealSpace
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & not lower_bound a <= b1 ) } is set
H is V11() real ext-real Element of the carrier of R^1
x is V45() V46() V47() Element of K6( the carrier of R^1)
t is V11() real ext-real set
Ball (H0,t) is V45() V46() V47() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is set
(lower_bound a) + t is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
r is V11() real ext-real set
r is V11() real ext-real Element of REAL
(lower_bound a) - r is V11() real ext-real Element of REAL
- ((lower_bound a) - r) is V11() real ext-real Element of REAL
- t is V11() real ext-real set
r - (lower_bound a) is V11() real ext-real Element of REAL
abs (r - (lower_bound a)) is V11() real ext-real Element of REAL
the distance of RealSpace is V16() V19(K7( the carrier of RealSpace, the carrier of RealSpace)) V20( REAL ) Function-like V26(K7( the carrier of RealSpace, the carrier of RealSpace)) quasi_total Element of K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL))
K7( the carrier of RealSpace, the carrier of RealSpace) is set
K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL) is set
K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL)) is set
p is V11() real ext-real Element of the carrier of RealSpace
the distance of RealSpace . (p,H0) is V11() real ext-real Element of REAL
dist (H0,p) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of the carrier of RealSpace : not t <= dist (H0,b1) } is set
t is set
r is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
f \/ a is V45() V46() V47() Element of K6(REAL)
r is V45() V46() V47() Element of K6( the carrier of R^1)
H is V11() real ext-real Element of the carrier of R^1
r is V11() real ext-real set
Ball (H0,r) is V45() V46() V47() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is set
p is V11() real ext-real Element of REAL
p / 2 is V11() real ext-real Element of REAL
(lower_bound a) - (p / 2) is V11() real ext-real Element of REAL
max (0,((lower_bound a) - (p / 2))) is V11() real ext-real Element of REAL
p * 1 is V11() real ext-real Element of REAL
1 / 2 is V11() real ext-real non negative Element of REAL
p * (1 / 2) is V11() real ext-real Element of REAL
(lower_bound a) - (max (0,((lower_bound a) - (p / 2)))) is V11() real ext-real Element of REAL
abs ((lower_bound a) - (max (0,((lower_bound a) - (p / 2))))) is V11() real ext-real Element of REAL
w is V11() real ext-real Element of REAL
(lower_bound a) - (max (0,((lower_bound a) - (p / 2)))) is V11() real ext-real Element of REAL
abs ((lower_bound a) - (max (0,((lower_bound a) - (p / 2))))) is V11() real ext-real Element of REAL
(lower_bound a) - (max (0,((lower_bound a) - (p / 2)))) is V11() real ext-real Element of REAL
abs ((lower_bound a) - (max (0,((lower_bound a) - (p / 2))))) is V11() real ext-real Element of REAL
(lower_bound a) - (max (0,((lower_bound a) - (p / 2)))) is V11() real ext-real Element of REAL
abs ((lower_bound a) - (max (0,((lower_bound a) - (p / 2))))) is V11() real ext-real Element of REAL
the distance of RealSpace is V16() V19(K7( the carrier of RealSpace, the carrier of RealSpace)) V20( REAL ) Function-like V26(K7( the carrier of RealSpace, the carrier of RealSpace)) quasi_total Element of K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL))
K7( the carrier of RealSpace, the carrier of RealSpace) is set
K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL) is set
K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL)) is set
W0 is V11() real ext-real Element of the carrier of RealSpace
the distance of RealSpace . (H0,W0) is V11() real ext-real Element of REAL
dist (H0,W0) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of the carrier of RealSpace : not p <= dist (H0,b1) } is set
Ball (H0,p) is V45() V46() V47() Element of K6( the carrier of RealSpace)
w is V11() real ext-real Element of REAL
t is V45() V46() V47() Element of K6( the carrier of R^1)
Cl t is V45() V46() V47() Element of K6( the carrier of R^1)
Cl y is V45() V46() V47() Element of K6( the carrier of R^1)
y ` is V45() V46() V47() Element of K6( the carrier of R^1)
the carrier of R^1 \ y is V45() V46() V47() set
lower_bound f is V11() real ext-real Element of REAL
H0 is V11() real ext-real Element of the carrier of RealSpace
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & not lower_bound f <= b1 ) } is set
H is V11() real ext-real Element of the carrier of R^1
x is V45() V46() V47() Element of K6( the carrier of R^1)
t is V11() real ext-real set
Ball (H0,t) is V45() V46() V47() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is set
(lower_bound f) + t is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
r is V11() real ext-real set
r is V11() real ext-real Element of REAL
(lower_bound f) - r is V11() real ext-real Element of REAL
- ((lower_bound f) - r) is V11() real ext-real Element of REAL
- t is V11() real ext-real set
r - (lower_bound f) is V11() real ext-real Element of REAL
abs (r - (lower_bound f)) is V11() real ext-real Element of REAL
real_dist . (r,(lower_bound f)) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of the carrier of RealSpace
dist (p,H0) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of the carrier of RealSpace : not t <= dist (H0,b1) } is set
t is set
r is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
f \/ a is V45() V46() V47() Element of K6(REAL)
r is V45() V46() V47() Element of K6( the carrier of R^1)
H is V11() real ext-real Element of the carrier of R^1
r is V11() real ext-real set
Ball (H0,r) is V45() V46() V47() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is set
p is V11() real ext-real Element of REAL
p / 2 is V11() real ext-real Element of REAL
(lower_bound f) - (p / 2) is V11() real ext-real Element of REAL
max (0,((lower_bound f) - (p / 2))) is V11() real ext-real Element of REAL
p * 1 is V11() real ext-real Element of REAL
1 / 2 is V11() real ext-real non negative Element of REAL
p * (1 / 2) is V11() real ext-real Element of REAL
(lower_bound f) - (max (0,((lower_bound f) - (p / 2)))) is V11() real ext-real Element of REAL
abs ((lower_bound f) - (max (0,((lower_bound f) - (p / 2))))) is V11() real ext-real Element of REAL
w is V11() real ext-real Element of REAL
(lower_bound f) - (max (0,((lower_bound f) - (p / 2)))) is V11() real ext-real Element of REAL
abs ((lower_bound f) - (max (0,((lower_bound f) - (p / 2))))) is V11() real ext-real Element of REAL
(lower_bound f) - (max (0,((lower_bound f) - (p / 2)))) is V11() real ext-real Element of REAL
abs ((lower_bound f) - (max (0,((lower_bound f) - (p / 2))))) is V11() real ext-real Element of REAL
(lower_bound f) - (max (0,((lower_bound f) - (p / 2)))) is V11() real ext-real Element of REAL
abs ((lower_bound f) - (max (0,((lower_bound f) - (p / 2))))) is V11() real ext-real Element of REAL
real_dist . ((lower_bound f),(max (0,((lower_bound f) - (p / 2))))) is V11() real ext-real Element of REAL
W0 is V11() real ext-real Element of the carrier of RealSpace
dist (H0,W0) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of the carrier of RealSpace : not p <= dist (H0,b1) } is set
Ball (H0,p) is V45() V46() V47() Element of K6( the carrier of RealSpace)
w is V11() real ext-real Element of REAL
t is V45() V46() V47() Element of K6( the carrier of R^1)
Cl t is V45() V46() V47() Element of K6( the carrier of R^1)
Cl x is V45() V46() V47() Element of K6( the carrier of R^1)
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y,(X,Y),(X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
rng (X,Y,(X,Y),(X,Y)) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
K6( the carrier of (Closed-Interval-TSpace (X,Y))) is set
[#] (Closed-Interval-TSpace (X,Y)) is non empty non proper V45() V46() V47() closed Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
[#] (Closed-Interval-TSpace (0,1)) is non empty non proper V45() V46() V47() closed Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
K6( the carrier of (Closed-Interval-TSpace (0,1))) is set
(X,Y,(X,Y),(X,Y)) .: the carrier of (Closed-Interval-TSpace (0,1)) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
[.X,Y.] is V45() V46() V47() Element of K6(REAL)
{X} is non empty V45() V46() V47() Element of K6(REAL)
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
[#] (Closed-Interval-TSpace (X,Y)) is non empty non proper V45() V46() V47() closed Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
K6( the carrier of (Closed-Interval-TSpace (X,Y))) is set
{(X,Y)} is non empty V45() V46() V47() connected Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
K7( the carrier of I[01], the carrier of I[01]) is set
K6(K7( the carrier of I[01], the carrier of I[01])) is set
X is non empty V16() V19( the carrier of I[01]) V20( the carrier of I[01]) Function-like V26( the carrier of I[01]) quasi_total continuous Element of K6(K7( the carrier of I[01], the carrier of I[01]))
K7([.0,1.],[.0,1.]) is set
K6(K7([.0,1.],[.0,1.])) is set
Y is V16() V19([.0,1.]) V20([.0,1.]) Function-like V26([.0,1.]) quasi_total Element of K6(K7([.0,1.],[.0,1.]))
{ b1 where b1 is V11() real ext-real Element of REAL : ( b1 in [.0,1.] & Y . b1 in [.0,b1.] ) } is set
{ b1 where b1 is V11() real ext-real Element of REAL : ( b1 in [.0,1.] & Y . b1 in [.b1,1.] ) } is set
b is set
g is V11() real ext-real Element of REAL
Y . g is set
[.0,g.] is V45() V46() V47() Element of K6(REAL)
Closed-Interval-MSpace (0,1) is non empty strict Reflexive discerning symmetric triangle Discerning SubSpace of RealSpace
TopSpaceMetr (Closed-Interval-MSpace (0,1)) is TopStruct
b is V45() V46() V47() Element of K6(REAL)
g is set
B is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
Y . x is set
[.0,x.] is V45() V46() V47() Element of K6(REAL)
g is set
B is V11() real ext-real Element of REAL
Y . B is set
[.B,1.] is V45() V46() V47() Element of K6(REAL)
the carrier of (Closed-Interval-MSpace (0,1)) is non empty set
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
dom Y is V45() V46() V47() Element of K6([.0,1.])
K6([.0,1.]) is set
Y . 0 is set
rng Y is V45() V46() V47() Element of K6([.0,1.])
g is V45() V46() V47() Element of K6(REAL)
b \/ g is V45() V46() V47() Element of K6(REAL)
B is set
x is V11() real ext-real Element of REAL
[.0,x.] is V45() V46() V47() Element of K6(REAL)
[.x,1.] is V45() V46() V47() Element of K6(REAL)
[.0,x.] \/ [.x,1.] is V45() V46() V47() Element of K6(REAL)
y is V11() real ext-real Element of REAL
Y . x is set
B is set
x is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
Y . y is set
[.y,1.] is V45() V46() V47() Element of K6(REAL)
b /\ g is V45() V46() V47() Element of K6(REAL)
the V11() real ext-real Element of b /\ g is V11() real ext-real Element of b /\ g
x is V11() real ext-real Element of REAL
Y . x is set
[.0,x.] is V45() V46() V47() Element of K6(REAL)
[.x,1.] is V45() V46() V47() Element of K6(REAL)
[.0,x.] /\ [.x,1.] is V45() V46() V47() Element of K6(REAL)
y is V11() real ext-real Element of REAL
Y . y is set
[.y,1.] is V45() V46() V47() Element of K6(REAL)
x is V11() real ext-real Element of REAL
Y . x is set
[.0,x.] is V45() V46() V47() Element of K6(REAL)
y is V11() real ext-real Element of REAL
Y . y is set
[.0,y.] is V45() V46() V47() Element of K6(REAL)
{x} is non empty V45() V46() V47() Element of K6(REAL)
y is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
Y . y is set
[.0,y.] is V45() V46() V47() Element of K6(REAL)
Y . 1 is set
K6( the carrier of I[01]) is set
[#] I[01] is non empty non proper V45() V46() V47() closed Element of K6( the carrier of I[01])
{} I[01] is empty V45() V46() V47() V48() V49() V50() V51() closed connected Element of K6( the carrier of I[01])
B is V45() V46() V47() Element of K6( the carrier of I[01])
x is V45() V46() V47() Element of K6( the carrier of I[01])
B \/ x is V45() V46() V47() Element of K6( the carrier of I[01])
Cl B is V45() V46() V47() Element of K6( the carrier of I[01])
(Cl B) /\ x is V45() V46() V47() Element of K6( the carrier of I[01])
the V11() real ext-real Element of (Cl B) /\ x is V11() real ext-real Element of (Cl B) /\ x
x ` is V45() V46() V47() Element of K6( the carrier of I[01])
the carrier of I[01] \ x is V45() V46() V47() set
x is V11() real ext-real Element of the carrier of I[01]
x is V11() real ext-real Element of REAL
Y . x is set
H0 is V11() real ext-real Element of REAL
Y . H0 is set
[.H0,1.] is V45() V46() V47() Element of K6(REAL)
x is V11() real ext-real Element of REAL
H0 is V11() real ext-real Element of REAL
Y . H0 is set
[.H0,1.] is V45() V46() V47() Element of K6(REAL)
x - x is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative Element of REAL
(x - x) * (2 ") is V11() real ext-real Element of REAL
X . x is V11() real ext-real Element of the carrier of I[01]
H is Element of the carrier of (Closed-Interval-MSpace (0,1))
Ball (H,((x - x) * (2 "))) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
K6( the carrier of (Closed-Interval-MSpace (0,1))) is set
t is V45() V46() V47() Element of K6( the carrier of I[01])
(x - x) / 2 is V11() real ext-real Element of REAL
0 / 2 is empty V11() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() Element of REAL
r is V45() V46() V47() Element of K6( the carrier of I[01])
X .: r is V45() V46() V47() Element of K6( the carrier of I[01])
H is Element of the carrier of (Closed-Interval-MSpace (0,1))
r is V11() real ext-real set
Ball (H,r) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
p is V11() real ext-real Element of REAL
min (p,((x - x) * (2 "))) is V11() real ext-real Element of REAL
Ball (H,(min (p,((x - x) * (2 "))))) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
W0 is V45() V46() V47() Element of K6( the carrier of I[01])
B /\ W0 is V45() V46() V47() Element of K6( the carrier of I[01])
the V11() real ext-real Element of B /\ W0 is V11() real ext-real Element of B /\ W0
w is Element of the carrier of (Closed-Interval-MSpace (0,1))
w1 is V11() real ext-real Element of the carrier of I[01]
d is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of (Closed-Interval-MSpace (0,1)) : not min (p,((x - x) * (2 "))) <= dist (H,b1) } is set
dist (w,H) is V11() real ext-real Element of REAL
x is Element of the carrier of (Closed-Interval-MSpace (0,1))
dist (H,x) is V11() real ext-real Element of REAL
d - x is V11() real ext-real Element of REAL
abs (d - x) is V11() real ext-real Element of REAL
x + ((x - x) * (2 ")) is V11() real ext-real Element of REAL
x - ((x - x) * (2 ")) is V11() real ext-real Element of REAL
(x - x) * 1 is V11() real ext-real Element of REAL
[.x,1.] is V45() V46() V47() Element of K6(REAL)
x is set
{ b1 where b1 is Element of the carrier of (Closed-Interval-MSpace (0,1)) : not (x - x) * (2 ") <= dist (H,b1) } is set
v is Element of the carrier of (Closed-Interval-MSpace (0,1))
t is V11() real ext-real Element of REAL
x - t is V11() real ext-real Element of REAL
abs (x - t) is V11() real ext-real Element of REAL
c29 is Element of the carrier of (Closed-Interval-MSpace (0,1))
dist (H,c29) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( x <= b1 & b1 <= 1 ) } is set
[.d,1.] is V45() V46() V47() Element of K6(REAL)
x is set
{ b1 where b1 is Element of the carrier of (Closed-Interval-MSpace (0,1)) : not (x - x) * (2 ") <= dist (H,b1) } is set
v is Element of the carrier of (Closed-Interval-MSpace (0,1))
t is V11() real ext-real Element of REAL
x - t is V11() real ext-real Element of REAL
abs (x - t) is V11() real ext-real Element of REAL
c29 is Element of the carrier of (Closed-Interval-MSpace (0,1))
dist (H,c29) is V11() real ext-real Element of REAL
((x - x) * (2 ")) + t is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( d <= b1 & b1 <= 1 ) } is set
Ball (H,p) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
X . w1 is V11() real ext-real Element of the carrier of I[01]
Cl x is V45() V46() V47() Element of K6( the carrier of I[01])
(Cl x) /\ B is V45() V46() V47() Element of K6( the carrier of I[01])
the V11() real ext-real Element of (Cl x) /\ B is V11() real ext-real Element of (Cl x) /\ B
B ` is V45() V46() V47() Element of K6( the carrier of I[01])
the carrier of I[01] \ B is V45() V46() V47() set
x is V11() real ext-real Element of the carrier of I[01]
x is V11() real ext-real Element of REAL
Y . x is set
H0 is V11() real ext-real Element of REAL
Y . H0 is set
[.0,H0.] is V45() V46() V47() Element of K6(REAL)
x is V11() real ext-real Element of REAL
H0 is V11() real ext-real Element of REAL
Y . H0 is set
[.0,H0.] is V45() V46() V47() Element of K6(REAL)
x - x is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative Element of REAL
(x - x) * (2 ") is V11() real ext-real Element of REAL
X . x is V11() real ext-real Element of the carrier of I[01]
H is Element of the carrier of (Closed-Interval-MSpace (0,1))
Ball (H,((x - x) * (2 "))) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
K6( the carrier of (Closed-Interval-MSpace (0,1))) is set
t is V45() V46() V47() Element of K6( the carrier of I[01])
(x - x) / 2 is V11() real ext-real Element of REAL
0 / 2 is empty V11() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() Element of REAL
r is V45() V46() V47() Element of K6( the carrier of I[01])
X .: r is V45() V46() V47() Element of K6( the carrier of I[01])
H is Element of the carrier of (Closed-Interval-MSpace (0,1))
r is V11() real ext-real set
Ball (H,r) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
p is V11() real ext-real Element of REAL
min (p,((x - x) * (2 "))) is V11() real ext-real Element of REAL
Ball (H,(min (p,((x - x) * (2 "))))) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
W0 is V45() V46() V47() Element of K6( the carrier of I[01])
x /\ W0 is V45() V46() V47() Element of K6( the carrier of I[01])
the V11() real ext-real Element of x /\ W0 is V11() real ext-real Element of x /\ W0
w is Element of the carrier of (Closed-Interval-MSpace (0,1))
w1 is V11() real ext-real Element of the carrier of I[01]
d is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of (Closed-Interval-MSpace (0,1)) : not min (p,((x - x) * (2 "))) <= dist (H,b1) } is set
dist (H,w) is V11() real ext-real Element of REAL
x is Element of the carrier of (Closed-Interval-MSpace (0,1))
dist (H,x) is V11() real ext-real Element of REAL
x - d is V11() real ext-real Element of REAL
abs (x - d) is V11() real ext-real Element of REAL
- d is V11() real ext-real Element of REAL
x + (- d) is V11() real ext-real Element of REAL
((x - x) * (2 ")) - (- d) is V11() real ext-real Element of REAL
x + ((x - x) * (2 ")) is V11() real ext-real Element of REAL
x - ((x - x) * (2 ")) is V11() real ext-real Element of REAL
- (- d) is V11() real ext-real Element of REAL
((x - x) * (2 ")) + (- (- d)) is V11() real ext-real Element of REAL
(x - x) * 1 is V11() real ext-real Element of REAL
[.0,x.] is V45() V46() V47() Element of K6(REAL)
x is set
{ b1 where b1 is Element of the carrier of (Closed-Interval-MSpace (0,1)) : not (x - x) * (2 ") <= dist (H,b1) } is set
v is Element of the carrier of (Closed-Interval-MSpace (0,1))
t is V11() real ext-real Element of REAL
t - x is V11() real ext-real Element of REAL
abs (t - x) is V11() real ext-real Element of REAL
c29 is Element of the carrier of (Closed-Interval-MSpace (0,1))
dist (H,c29) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= x ) } is set
[.0,d.] is V45() V46() V47() Element of K6(REAL)
x is set
{ b1 where b1 is Element of the carrier of (Closed-Interval-MSpace (0,1)) : not (x - x) * (2 ") <= dist (H,b1) } is set
v is Element of the carrier of (Closed-Interval-MSpace (0,1))
t is V11() real ext-real Element of REAL
t - x is V11() real ext-real Element of REAL
abs (t - x) is V11() real ext-real Element of REAL
c29 is Element of the carrier of (Closed-Interval-MSpace (0,1))
dist (H,c29) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= d ) } is set
Ball (H,p) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
X . w1 is V11() real ext-real Element of the carrier of I[01]
B is V45() V46() V47() Element of K6( the carrier of I[01])
x is V45() V46() V47() Element of K6( the carrier of I[01])
B \/ x is V45() V46() V47() Element of K6( the carrier of I[01])
X is V11() real ext-real set
Y is V11() real ext-real set
Closed-Interval-TSpace (X,Y) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V45() V46() V47() set
K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
f is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total continuous Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(X,Y,(X,Y),(X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y)))) is set
(X,Y,(0,1),(0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1)))) is set
(X,Y,(0,1),(0,1)) * f is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
((X,Y,(0,1),(0,1)) * f) * (X,Y,(X,Y),(X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))))
id (Closed-Interval-TSpace (X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
id the carrier of (Closed-Interval-TSpace (X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
(X,Y,(X,Y),(X,Y)) * (X,Y,(0,1),(0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
((X,Y,(X,Y),(X,Y)) * (X,Y,(0,1),(0,1))) * f is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
(X,Y,(X,Y),(X,Y)) * ((X,Y,(0,1),(0,1)) * f) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
((X,Y,(0,1),(0,1)) * f) * ((X,Y,(X,Y),(X,Y)) * (X,Y,(0,1),(0,1))) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
(X,Y,(X,Y),(X,Y)) * (((X,Y,(0,1),(0,1)) * f) * ((X,Y,(X,Y),(X,Y)) * (X,Y,(0,1),(0,1)))) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
(((X,Y,(0,1),(0,1)) * f) * (X,Y,(X,Y),(X,Y))) * (X,Y,(0,1),(0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (0,1))))
(X,Y,(X,Y),(X,Y)) * ((((X,Y,(0,1),(0,1)) * f) * (X,Y,(X,Y),(X,Y))) * (X,Y,(0,1),(0,1))) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
(X,Y,(X,Y),(X,Y)) * (((X,Y,(0,1),(0,1)) * f) * (X,Y,(X,Y),(X,Y))) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
((X,Y,(X,Y),(X,Y)) * (((X,Y,(0,1),(0,1)) * f) * (X,Y,(X,Y),(X,Y)))) * (X,Y,(0,1),(0,1)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (X,Y))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (X,Y))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (X,Y)), the carrier of (Closed-Interval-TSpace (X,Y))))
B is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(((X,Y,(0,1),(0,1)) * f) * (X,Y,(X,Y),(X,Y))) . B is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(X,Y,(0,1),(0,1)) * (X,Y,(X,Y),(X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (0,1))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))))
(X,Y,(X,Y),(X,Y)) . B is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
x is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
f . x is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
(((X,Y,(X,Y),(X,Y)) * (((X,Y,(0,1),(0,1)) * f) * (X,Y,(X,Y),(X,Y)))) * (X,Y,(0,1),(0,1))) * (X,Y,(X,Y),(X,Y)) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
((((X,Y,(X,Y),(X,Y)) * (((X,Y,(0,1),(0,1)) * f) * (X,Y,(X,Y),(X,Y)))) * (X,Y,(0,1),(0,1))) * (X,Y,(X,Y),(X,Y))) . B is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
((X,Y,(X,Y),(X,Y)) * (((X,Y,(0,1),(0,1)) * f) * (X,Y,(X,Y),(X,Y)))) * (id (Closed-Interval-TSpace (0,1))) is non empty V16() V19( the carrier of (Closed-Interval-TSpace (0,1))) V20( the carrier of (Closed-Interval-TSpace (X,Y))) Function-like V26( the carrier of (Closed-Interval-TSpace (0,1))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (X,Y))))
(((X,Y,(X,Y),(X,Y)) * (((X,Y,(0,1),(0,1)) * f) * (X,Y,(X,Y),(X,Y)))) * (id (Closed-Interval-TSpace (0,1)))) . B is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
((X,Y,(X,Y),(X,Y)) * (((X,Y,(0,1),(0,1)) * f) * (X,Y,(X,Y),(X,Y)))) . B is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
x is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
f . x is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
[.X,Y.] is V45() V46() V47() Element of K6(REAL)
{X} is non empty V45() V46() V47() Element of K6(REAL)
(X,Y) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
{(X,Y)} is non empty V45() V46() V47() connected Element of K6( the carrier of (Closed-Interval-TSpace (X,Y)))
K6( the carrier of (Closed-Interval-TSpace (X,Y))) is set
a is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
f . a is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
a is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
f . a is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
a is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
f . a is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (X,Y))
X is non empty TopSpace-like V146() SubSpace of R^1
the carrier of X is non empty V45() V46() V47() set
Y is non empty TopSpace-like V146() SubSpace of R^1
the carrier of Y is non empty V45() V46() V47() set
K7( the carrier of X, the carrier of Y) is set
K6(K7( the carrier of X, the carrier of Y)) is set
f is non empty V16() V19( the carrier of X) V20( the carrier of Y) Function-like V26( the carrier of X) quasi_total continuous Element of K6(K7( the carrier of X, the carrier of Y))
a is V11() real ext-real Element of REAL
b is V11() real ext-real Element of REAL
[.a,b.] is V45() V46() V47() Element of K6(REAL)
f .: [.a,b.] is V45() V46() V47() Element of K6( the carrier of Y)
K6( the carrier of Y) is set
K6( the carrier of X) is set
g is non empty V45() V46() V47() Element of K6( the carrier of X)
f | g is V16() V19( the carrier of X) V20( the carrier of Y) Function-like Element of K6(K7( the carrier of X, the carrier of Y))
dom (f | g) is V45() V46() V47() Element of K6( the carrier of X)
dom f is V45() V46() V47() Element of K6( the carrier of X)
(dom f) /\ g is V45() V46() V47() Element of K6( the carrier of X)
the carrier of X /\ g is V45() V46() V47() Element of K6( the carrier of X)
Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like V146() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (a,b)) is non empty V45() V46() V47() set
rng (f | g) is V45() V46() V47() Element of K6( the carrier of Y)
K7( the carrier of (Closed-Interval-TSpace (a,b)), the carrier of (Closed-Interval-TSpace (a,b))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (a,b)), the carrier of (Closed-Interval-TSpace (a,b)))) is set
B is TopSpace-like V146() SubSpace of X
x is non empty V16() V19( the carrier of (Closed-Interval-TSpace (a,b))) V20( the carrier of (Closed-Interval-TSpace (a,b))) Function-like V26( the carrier of (Closed-Interval-TSpace (a,b))) quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (a,b)), the carrier of (Closed-Interval-TSpace (a,b))))
y is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (a,b))
K6( the carrier of (Closed-Interval-TSpace (a,b))) is set
x . y is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (a,b))
the carrier of B is V45() V46() V47() set
K6( the carrier of B) is set
x is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (a,b)))
x is V11() real ext-real Element of the carrier of X
[#] (Closed-Interval-TSpace (a,b)) is non empty non proper V45() V46() V47() closed Element of K6( the carrier of (Closed-Interval-TSpace (a,b)))
x is V45() V46() V47() Element of K6( the carrier of Y)
x /\ ([#] (Closed-Interval-TSpace (a,b))) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (a,b)))
f . x is V11() real ext-real Element of the carrier of Y
H0 is V45() V46() V47() Element of K6( the carrier of X)
f .: H0 is V45() V46() V47() Element of K6( the carrier of Y)
H0 /\ ([#] (Closed-Interval-TSpace (a,b))) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (a,b)))
H is V45() V46() V47() Element of K6( the carrier of B)
H is V45() V46() V47() Element of K6( the carrier of B)
x .: H is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (a,b)))
t is set
dom x is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (a,b)))
r is set
x . r is set
r is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (a,b))
x .: the carrier of B is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (a,b)))
p is V11() real ext-real Element of the carrier of X
[#] X is non empty non proper V45() V46() V47() closed Element of K6( the carrier of X)
f . p is V11() real ext-real Element of the carrier of Y
H is V45() V46() V47() Element of K6( the carrier of B)
x .: H is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (a,b)))
y is non empty V16() V19( the carrier of (Closed-Interval-TSpace (a,b))) V20( the carrier of (Closed-Interval-TSpace (a,b))) Function-like V26( the carrier of (Closed-Interval-TSpace (a,b))) quasi_total continuous Element of K6(K7( the carrier of (Closed-Interval-TSpace (a,b)), the carrier of (Closed-Interval-TSpace (a,b))))
x is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (a,b))
y . x is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (a,b))
x is V11() real ext-real Element of the carrier of X
x is V11() real ext-real Element of the carrier of X
f . x is V11() real ext-real Element of the carrier of Y
x is V11() real ext-real Element of the carrier of X
f . x is V11() real ext-real Element of the carrier of Y
X is non empty TopSpace-like V146() SubSpace of R^1
the carrier of X is non empty V45() V46() V47() set
Y is non empty TopSpace-like V146() SubSpace of R^1
the carrier of Y is non empty V45() V46() V47() set
K7( the carrier of X, the carrier of Y) is set
K6(K7( the carrier of X, the carrier of Y)) is set
f is non empty V16() V19( the carrier of X) V20( the carrier of Y) Function-like V26( the carrier of X) quasi_total continuous Element of K6(K7( the carrier of X, the carrier of Y))
a is V11() real ext-real Element of REAL
b is V11() real ext-real Element of REAL
[.a,b.] is V45() V46() V47() Element of K6(REAL)
f .: [.a,b.] is V45() V46() V47() Element of K6( the carrier of Y)
K6( the carrier of Y) is set
incl Y is non empty V16() V19( the carrier of Y) V20( the carrier of R^1) Function-like V26( the carrier of Y) quasi_total Element of K6(K7( the carrier of Y, the carrier of R^1))
K7( the carrier of Y, the carrier of R^1) is set
K6(K7( the carrier of Y, the carrier of R^1)) is set
(incl Y) * f is non empty V16() V19( the carrier of X) V20( the carrier of R^1) Function-like V26( the carrier of X) quasi_total Element of K6(K7( the carrier of X, the carrier of R^1))
K7( the carrier of X, the carrier of R^1) is set
K6(K7( the carrier of X, the carrier of R^1)) is set
((incl Y) * f) .: [.a,b.] is V45() V46() V47() Element of K6( the carrier of R^1)
(incl Y) .: (f .: [.a,b.]) is V45() V46() V47() Element of K6( the carrier of R^1)
id R^1 is non empty V16() V19( the carrier of R^1) V20( the carrier of R^1) Function-like V26( the carrier of R^1) quasi_total Element of K6(K7( the carrier of R^1, the carrier of R^1))
id the carrier of R^1 is non empty V16() V19( the carrier of R^1) V20( the carrier of R^1) V26( the carrier of R^1) quasi_total Element of K6(K7( the carrier of R^1, the carrier of R^1))
(id R^1) | Y is non empty V16() V19( the carrier of Y) V20( the carrier of R^1) Function-like V26( the carrier of Y) quasi_total Element of K6(K7( the carrier of Y, the carrier of R^1))
B is V45() V46() V47() Element of K6( the carrier of R^1)
((id R^1) | Y) .: B is V45() V46() V47() Element of K6( the carrier of R^1)
(id R^1) .: B is V45() V46() V47() Element of K6( the carrier of R^1)
x is V11() real ext-real Element of the carrier of X
((incl Y) * f) . x is V11() real ext-real Element of the carrier of R^1
f . x is V11() real ext-real Element of the carrier of Y
x is V11() real ext-real Element of the carrier of X
f . x is V11() real ext-real Element of the carrier of Y
y is V11() real ext-real Element of the carrier of R^1
(incl Y) . y is set
x is V11() real ext-real Element of the carrier of X
f . x is V11() real ext-real Element of the carrier of Y