REAL is non empty V34() set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V34() set
omega is non empty epsilon-transitive epsilon-connected ordinal set
bool omega is non empty set
bool NAT is non empty set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() real ext-real positive non negative Element of NAT
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V27() real ext-real positive non negative Element of NAT
[:2,2:] is non empty set
[:[:2,2:],REAL:] is non empty set
bool [:[:2,2:],REAL:] is non empty set
[:NAT,REAL:] is non empty set
bool [:NAT,REAL:] is non empty set
RAT is non empty V34() set
INT is non empty V34() set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real ext-real non positive non negative set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real ext-real non positive non negative Element of NAT
X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
[:NAT,(bool the carrier of X):] is non empty set
bool [:NAT,(bool the carrier of X):] is non empty set
Family_open_set X is Element of bool (bool the carrier of X)
Y is V10() V13( NAT ) V14( bool the carrier of X) Function-like V46( NAT , bool the carrier of X) Element of bool [:NAT,(bool the carrier of X):]
rng Y is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
union (rng Y) is Element of bool the carrier of X
the Element of the carrier of X is Element of the carrier of X
Y . 0 is Element of bool the carrier of X
(Y . 0) ` is Element of bool the carrier of X
the carrier of X \ (Y . 0) is set
((Y . 0) `) ` is Element of bool the carrier of X
the carrier of X \ ((Y . 0) `) is set
the carrier of X \ ((Y . 0) `) is Element of bool the carrier of X
Ball ( the Element of the carrier of X,1) is Element of bool the carrier of X
f is set
ft is Element of the carrier of X
x is V27() real ext-real Element of REAL
Ball (ft,x) is Element of bool the carrier of X
1 / 2 is V27() real ext-real non negative Element of REAL
min (x,(1 / 2)) is V27() real ext-real Element of REAL
xt is V27() real ext-real Element of REAL
1 / 1 is V27() real ext-real non negative Element of REAL
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ 0) is V27() real ext-real Element of REAL
Ball (ft,xt) is Element of bool the carrier of X
(Ball (ft,xt)) /\ (Y . 0) is Element of bool the carrier of X
G is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
2 |^ G is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ G) is V27() real ext-real Element of REAL
Y . G is Element of bool the carrier of X
G + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
2 |^ (G + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ (G + 1)) is V27() real ext-real Element of REAL
Y . (G + 1) is Element of bool the carrier of X
Gt is Element of the carrier of X
Ht is V27() real ext-real Element of REAL
Ball (Gt,Ht) is Element of bool the carrier of X
(Ball (Gt,Ht)) /\ (Y . G) is Element of bool the carrier of X
Ht / 2 is V27() real ext-real Element of REAL
Ball (Gt,(Ht / 2)) is Element of bool the carrier of X
G + 2 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
2 |^ (G + 2) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ (G + 2)) is V27() real ext-real Element of REAL
(1 / (2 |^ (G + 1))) / 2 is V27() real ext-real Element of REAL
(G + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
2 |^ ((G + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
(2 |^ (G + 1)) * 2 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
(Y . (G + 1)) ` is Element of bool the carrier of X
the carrier of X \ (Y . (G + 1)) is set
(Ball (Gt,(Ht / 2))) /\ ((Y . (G + 1)) `) is Element of bool the carrier of X
H is set
H is Element of the carrier of X
s is V27() real ext-real Element of REAL
Ball (H,s) is Element of bool the carrier of X
w is V27() real ext-real Element of REAL
Ball (H,w) is Element of bool the carrier of X
min (w,s) is V27() real ext-real Element of REAL
min ((min (w,s)),(1 / (2 |^ (G + 2)))) is V27() real ext-real Element of REAL
v is V27() real ext-real Element of REAL
Ball (H,v) is Element of bool the carrier of X
w1 is V27() real ext-real Element of REAL
v1 is Element of the carrier of X
Ball (v1,w1) is Element of bool the carrier of X
(Ball (v1,w1)) /\ (Y . (G + 1)) is Element of bool the carrier of X
H is V27() real ext-real Element of REAL
H is Element of the carrier of X
Ball (H,H) is Element of bool the carrier of X
(Ball (H,H)) /\ (Y . (G + 1)) is Element of bool the carrier of X
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
[: the carrier of X,REAL:] is non empty set
G is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
2 |^ G is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ G) is V27() real ext-real Element of REAL
Y . G is Element of bool the carrier of X
G + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
2 |^ (G + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ (G + 1)) is V27() real ext-real Element of REAL
Y . (G + 1) is Element of bool the carrier of X
Gt is Element of [: the carrier of X,REAL:]
Gt `2 is V27() real ext-real Element of REAL
Gt `1 is Element of the carrier of X
Ball ((Gt `1),(Gt `2)) is Element of bool the carrier of X
(Ball ((Gt `1),(Gt `2))) /\ (Y . G) is Element of bool the carrier of X
(Gt `2) / 2 is V27() real ext-real Element of REAL
Ball ((Gt `1),((Gt `2) / 2)) is Element of bool the carrier of X
Ht is Element of the carrier of X
H is V27() real ext-real Element of REAL
Ball (Ht,H) is Element of bool the carrier of X
(Ball (Ht,H)) /\ (Y . (G + 1)) is Element of bool the carrier of X
[Ht,H] is Element of [: the carrier of X,REAL:]
{Ht,H} is non empty set
{Ht} is non empty set
{{Ht,H},{Ht}} is non empty set
[Ht,H] `2 is V27() real ext-real Element of REAL
[Ht,H] `1 is Element of the carrier of X
Ball (([Ht,H] `1),([Ht,H] `2)) is Element of bool the carrier of X
(Ball (([Ht,H] `1),([Ht,H] `2))) /\ (Y . (G + 1)) is Element of bool the carrier of X
[:NAT,[: the carrier of X,REAL:]:] is non empty set
bool [:NAT,[: the carrier of X,REAL:]:] is non empty set
[ft,xt] is Element of [: the carrier of X,REAL:]
{ft,xt} is non empty set
{ft} is non empty set
{{ft,xt},{ft}} is non empty set
G is V10() V13( NAT ) V14([: the carrier of X,REAL:]) Function-like V46( NAT ,[: the carrier of X,REAL:]) Element of bool [:NAT,[: the carrier of X,REAL:]:]
G . 0 is Element of [: the carrier of X,REAL:]
pr1 G is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
(pr1 G) . 0 is Element of the carrier of X
pr2 G is V10() V13( NAT ) V14( REAL ) Function-like V46( NAT , REAL ) Element of bool [:NAT,REAL:]
(pr2 G) . 0 is V27() real ext-real Element of REAL
(G . 0) `1 is Element of the carrier of X
(G . 0) `2 is V27() real ext-real Element of REAL
Gt is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Gt + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . (Gt + 1) is Element of [: the carrier of X,REAL:]
(G . (Gt + 1)) `1 is Element of the carrier of X
(pr1 G) . (Gt + 1) is Element of the carrier of X
(G . (Gt + 1)) `2 is V27() real ext-real Element of REAL
(pr2 G) . (Gt + 1) is V27() real ext-real Element of REAL
G . Gt is Element of [: the carrier of X,REAL:]
(G . Gt) `1 is Element of the carrier of X
(pr1 G) . Gt is Element of the carrier of X
(G . Gt) `2 is V27() real ext-real Element of REAL
(pr2 G) . Gt is V27() real ext-real Element of REAL
2 |^ Gt is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ Gt) is V27() real ext-real Element of REAL
Ball (((pr1 G) . Gt),((pr2 G) . Gt)) is Element of bool the carrier of X
Y . Gt is Element of bool the carrier of X
(Ball (((pr1 G) . Gt),((pr2 G) . Gt))) /\ (Y . Gt) is Element of bool the carrier of X
2 |^ (Gt + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ (Gt + 1)) is V27() real ext-real Element of REAL
Ball (((pr1 G) . (Gt + 1)),((pr2 G) . (Gt + 1))) is Element of bool the carrier of X
((pr2 G) . Gt) / 2 is V27() real ext-real Element of REAL
Ball (((pr1 G) . Gt),(((pr2 G) . Gt) / 2)) is Element of bool the carrier of X
Y . (Gt + 1) is Element of bool the carrier of X
(Ball (((pr1 G) . (Gt + 1)),((pr2 G) . (Gt + 1)))) /\ (Y . (Gt + 1)) is Element of bool the carrier of X
G is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
G . 0 is Element of the carrier of X
Gt is V10() V13( NAT ) V14( REAL ) Function-like V46( NAT , REAL ) Element of bool [:NAT,REAL:]
Gt . 0 is V27() real ext-real Element of REAL
G is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
G . 0 is Element of the carrier of X
Gt is V10() V13( NAT ) V14( REAL ) Function-like V46( NAT , REAL ) Element of bool [:NAT,REAL:]
Gt . 0 is V27() real ext-real Element of REAL
Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Gt . Ht is V27() real ext-real Element of REAL
2 |^ Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ Ht) is V27() real ext-real Element of REAL
Ht + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . (Ht + 1) is Element of the carrier of X
Gt . (Ht + 1) is V27() real ext-real Element of REAL
Ball ((G . (Ht + 1)),(Gt . (Ht + 1))) is Element of bool the carrier of X
G . Ht is Element of the carrier of X
(Gt . Ht) / 2 is V27() real ext-real Element of REAL
Ball ((G . Ht),((Gt . Ht) / 2)) is Element of bool the carrier of X
Ball ((G . Ht),(Gt . Ht)) is Element of bool the carrier of X
Y . Ht is Element of bool the carrier of X
(Ball ((G . Ht),(Gt . Ht))) /\ (Y . Ht) is Element of bool the carrier of X
Y . (Ht + 1) is Element of bool the carrier of X
(Ball ((G . (Ht + 1)),(Gt . (Ht + 1)))) /\ (Y . (Ht + 1)) is Element of bool the carrier of X
2 |^ (Ht + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ (Ht + 1)) is V27() real ext-real Element of REAL
(Ht + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . ((Ht + 1) + 1) is Element of the carrier of X
Gt . ((Ht + 1) + 1) is V27() real ext-real Element of REAL
Ball ((G . ((Ht + 1) + 1)),(Gt . ((Ht + 1) + 1))) is Element of bool the carrier of X
(Gt . (Ht + 1)) / 2 is V27() real ext-real Element of REAL
Ball ((G . (Ht + 1)),((Gt . (Ht + 1)) / 2)) is Element of bool the carrier of X
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() real ext-real positive non negative Element of NAT
G . (0 + 1) is Element of the carrier of X
Gt . (0 + 1) is V27() real ext-real Element of REAL
Ball ((G . (0 + 1)),(Gt . (0 + 1))) is Element of bool the carrier of X
(Gt . 0) / 2 is V27() real ext-real Element of REAL
Ball ((G . 0),((Gt . 0) / 2)) is Element of bool the carrier of X
Ball ((G . 0),(Gt . 0)) is Element of bool the carrier of X
(Ball ((G . 0),(Gt . 0))) /\ (Y . 0) is Element of bool the carrier of X
Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . Ht is Element of the carrier of X
2 |^ Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ Ht) is V27() real ext-real Element of REAL
H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Ht + H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . (Ht + H) is Element of the carrier of X
dist ((G . (Ht + H)),(G . Ht)) is V27() real ext-real Element of REAL
the distance of X is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
the distance of X . ((G . (Ht + H)),(G . Ht)) is V27() real ext-real Element of REAL
2 |^ H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ H) is V27() real ext-real Element of REAL
1 - (1 / (2 |^ H)) is V27() real ext-real Element of REAL
(1 / (2 |^ Ht)) * (1 - (1 / (2 |^ H))) is V27() real ext-real Element of REAL
(Ht + H) + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . ((Ht + H) + 1) is Element of the carrier of X
dist ((G . ((Ht + H) + 1)),(G . (Ht + H))) is V27() real ext-real Element of REAL
the distance of X . ((G . ((Ht + H) + 1)),(G . (Ht + H))) is V27() real ext-real Element of REAL
(dist ((G . ((Ht + H) + 1)),(G . (Ht + H)))) + (dist ((G . (Ht + H)),(G . Ht))) is V27() real ext-real Element of REAL
(dist ((G . ((Ht + H) + 1)),(G . (Ht + H)))) + ((1 / (2 |^ Ht)) * (1 - (1 / (2 |^ H)))) is V27() real ext-real Element of REAL
Gt . ((Ht + H) + 1) is V27() real ext-real Element of REAL
dist ((G . ((Ht + H) + 1)),(G . ((Ht + H) + 1))) is V27() real ext-real Element of REAL
the distance of X . ((G . ((Ht + H) + 1)),(G . ((Ht + H) + 1))) is V27() real ext-real Element of REAL
Ball ((G . ((Ht + H) + 1)),(Gt . ((Ht + H) + 1))) is Element of bool the carrier of X
2 |^ (Ht + H) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ (Ht + H)) is V27() real ext-real Element of REAL
Gt . (Ht + H) is V27() real ext-real Element of REAL
(1 / (2 |^ (Ht + H))) / 2 is V27() real ext-real Element of REAL
(Gt . (Ht + H)) / 2 is V27() real ext-real Element of REAL
(2 |^ (Ht + H)) * 2 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / ((2 |^ (Ht + H)) * 2) is V27() real ext-real Element of REAL
2 |^ ((Ht + H) + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ ((Ht + H) + 1)) is V27() real ext-real Element of REAL
Ball ((G . (Ht + H)),((Gt . (Ht + H)) / 2)) is Element of bool the carrier of X
(1 / (2 |^ ((Ht + H) + 1))) + ((1 / (2 |^ Ht)) * (1 - (1 / (2 |^ H)))) is V27() real ext-real Element of REAL
H + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Ht + (H + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
2 |^ (Ht + (H + 1)) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
2 |^ (H + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
(2 |^ Ht) * (2 |^ (H + 1)) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
(2 |^ (H + 1)) / 1 is V27() real ext-real Element of REAL
(1 / (2 |^ Ht)) / ((2 |^ (H + 1)) / 1) is V27() real ext-real Element of REAL
1 / (2 |^ (H + 1)) is V27() real ext-real Element of REAL
(1 / (2 |^ Ht)) * (1 / (2 |^ (H + 1))) is V27() real ext-real Element of REAL
(1 / (2 |^ (H + 1))) - (1 / (2 |^ H)) is V27() real ext-real Element of REAL
1 + ((1 / (2 |^ (H + 1))) - (1 / (2 |^ H))) is V27() real ext-real Element of REAL
(1 / (2 |^ Ht)) * (1 + ((1 / (2 |^ (H + 1))) - (1 / (2 |^ H)))) is V27() real ext-real Element of REAL
(2 |^ H) * 2 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / ((2 |^ H) * 2) is V27() real ext-real Element of REAL
(1 / ((2 |^ H) * 2)) - (1 / (2 |^ H)) is V27() real ext-real Element of REAL
1 + ((1 / ((2 |^ H) * 2)) - (1 / (2 |^ H))) is V27() real ext-real Element of REAL
(1 / (2 |^ Ht)) * (1 + ((1 / ((2 |^ H) * 2)) - (1 / (2 |^ H)))) is V27() real ext-real Element of REAL
(1 / (2 |^ H)) / 2 is V27() real ext-real Element of REAL
((1 / (2 |^ H)) / 2) - (1 / (2 |^ H)) is V27() real ext-real Element of REAL
1 + (((1 / (2 |^ H)) / 2) - (1 / (2 |^ H))) is V27() real ext-real Element of REAL
(1 / (2 |^ Ht)) * (1 + (((1 / (2 |^ H)) / 2) - (1 / (2 |^ H)))) is V27() real ext-real Element of REAL
1 - ((1 / (2 |^ H)) / 2) is V27() real ext-real Element of REAL
(1 / (2 |^ Ht)) * (1 - ((1 / (2 |^ H)) / 2)) is V27() real ext-real Element of REAL
1 - (1 / ((2 |^ H) * 2)) is V27() real ext-real Element of REAL
(1 / (2 |^ Ht)) * (1 - (1 / ((2 |^ H) * 2))) is V27() real ext-real Element of REAL
dist ((G . ((Ht + H) + 1)),(G . Ht)) is V27() real ext-real Element of REAL
the distance of X . ((G . ((Ht + H) + 1)),(G . Ht)) is V27() real ext-real Element of REAL
G . (Ht + (H + 1)) is Element of the carrier of X
dist ((G . (Ht + (H + 1))),(G . Ht)) is V27() real ext-real Element of REAL
the distance of X . ((G . (Ht + (H + 1))),(G . Ht)) is V27() real ext-real Element of REAL
1 - (1 / (2 |^ (H + 1))) is V27() real ext-real Element of REAL
(1 / (2 |^ Ht)) * (1 - (1 / (2 |^ (H + 1)))) is V27() real ext-real Element of REAL
Ht + 0 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . (Ht + 0) is Element of the carrier of X
dist ((G . (Ht + 0)),(G . Ht)) is V27() real ext-real Element of REAL
the distance of X . ((G . (Ht + 0)),(G . Ht)) is V27() real ext-real Element of REAL
1 - (1 / (2 |^ 0)) is V27() real ext-real Element of REAL
(1 / (2 |^ Ht)) * (1 - (1 / (2 |^ 0))) is V27() real ext-real Element of REAL
H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Ht + H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . (Ht + H) is Element of the carrier of X
dist ((G . (Ht + H)),(G . Ht)) is V27() real ext-real Element of REAL
the distance of X . ((G . (Ht + H)),(G . Ht)) is V27() real ext-real Element of REAL
2 |^ H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ H) is V27() real ext-real Element of REAL
1 - (1 / (2 |^ H)) is V27() real ext-real Element of REAL
(1 / (2 |^ Ht)) * (1 - (1 / (2 |^ H))) is V27() real ext-real Element of REAL
Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Ht + H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . (Ht + H) is Element of the carrier of X
G . Ht is Element of the carrier of X
dist ((G . (Ht + H)),(G . Ht)) is V27() real ext-real Element of REAL
the distance of X is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
the distance of X . ((G . (Ht + H)),(G . Ht)) is V27() real ext-real Element of REAL
2 |^ Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ Ht) is V27() real ext-real Element of REAL
2 |^ H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ H) is V27() real ext-real Element of REAL
1 - (1 / (2 |^ H)) is V27() real ext-real Element of REAL
(1 / (2 |^ Ht)) * (1 - (1 / (2 |^ H))) is V27() real ext-real Element of REAL
1 - 0 is non empty V27() real ext-real positive non negative Element of REAL
(1 / (2 |^ Ht)) * 1 is V27() real ext-real Element of REAL
Ht is V27() real ext-real Element of REAL
H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
2 |^ H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ H) is V27() real ext-real Element of REAL
H + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
w is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
v is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real set
H + v is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
v1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
H + v1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
2 |^ H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / (2 |^ H) is V27() real ext-real Element of REAL
G . s is Element of the carrier of X
G . H is Element of the carrier of X
dist ((G . s),(G . H)) is V27() real ext-real Element of REAL
the distance of X . ((G . s),(G . H)) is V27() real ext-real Element of REAL
w1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real set
H + w1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
(2 |^ H) * 2 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
1 / ((2 |^ H) * 2) is V27() real ext-real Element of REAL
(1 / (2 |^ H)) / 2 is V27() real ext-real Element of REAL
zza is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
H + zza is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
(1 / (2 |^ H)) + (1 / (2 |^ H)) is V27() real ext-real Element of REAL
G . w is Element of the carrier of X
dist ((G . H),(G . w)) is V27() real ext-real Element of REAL
the distance of X . ((G . H),(G . w)) is V27() real ext-real Element of REAL
(dist ((G . s),(G . H))) + (dist ((G . H),(G . w))) is V27() real ext-real Element of REAL
dist ((G . s),(G . w)) is V27() real ext-real Element of REAL
the distance of X . ((G . s),(G . w)) is V27() real ext-real Element of REAL
Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Ht + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . Ht is Element of the carrier of X
Gt . Ht is V27() real ext-real Element of REAL
(Gt . Ht) / 2 is V27() real ext-real Element of REAL
Ball ((G . Ht),((Gt . Ht) / 2)) is Element of bool the carrier of X
H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
(Ht + 1) + H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . ((Ht + 1) + H) is Element of the carrier of X
Gt . ((Ht + 1) + H) is V27() real ext-real Element of REAL
Ball ((G . ((Ht + 1) + H)),(Gt . ((Ht + 1) + H))) is Element of bool the carrier of X
(Gt . ((Ht + 1) + H)) / 2 is V27() real ext-real Element of REAL
Ball ((G . ((Ht + 1) + H)),((Gt . ((Ht + 1) + H)) / 2)) is Element of bool the carrier of X
H + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
(Ht + 1) + (H + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . ((Ht + 1) + (H + 1)) is Element of the carrier of X
Gt . ((Ht + 1) + (H + 1)) is V27() real ext-real Element of REAL
Ball ((G . ((Ht + 1) + (H + 1))),(Gt . ((Ht + 1) + (H + 1)))) is Element of bool the carrier of X
((Ht + 1) + H) + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . (((Ht + 1) + H) + 1) is Element of the carrier of X
Gt . (((Ht + 1) + H) + 1) is V27() real ext-real Element of REAL
Ball ((G . (((Ht + 1) + H) + 1)),(Gt . (((Ht + 1) + H) + 1))) is Element of bool the carrier of X
(Ht + 1) + 0 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . ((Ht + 1) + 0) is Element of the carrier of X
Gt . ((Ht + 1) + 0) is V27() real ext-real Element of REAL
Ball ((G . ((Ht + 1) + 0)),(Gt . ((Ht + 1) + 0))) is Element of bool the carrier of X
Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Ht + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Gt . Ht is V27() real ext-real Element of REAL
(Gt . Ht) / 2 is V27() real ext-real Element of REAL
lim G is Element of the carrier of X
H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
max (H,(Ht + 1)) is V27() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . s is Element of the carrier of X
dist ((G . s),(lim G)) is V27() real ext-real Element of REAL
the distance of X . ((G . s),(lim G)) is V27() real ext-real Element of REAL
w is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real set
(Ht + 1) + w is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
dist ((G . s),(G . s)) is V27() real ext-real Element of REAL
the distance of X . ((G . s),(G . s)) is V27() real ext-real Element of REAL
Gt . s is V27() real ext-real Element of REAL
Ball ((G . s),(Gt . s)) is Element of bool the carrier of X
v is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
(Ht + 1) + v is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
G . Ht is Element of the carrier of X
Ball ((G . Ht),((Gt . Ht) / 2)) is Element of bool the carrier of X
dist ((G . s),(G . Ht)) is V27() real ext-real Element of REAL
the distance of X . ((G . s),(G . Ht)) is V27() real ext-real Element of REAL
((Gt . Ht) / 2) + ((Gt . Ht) / 2) is V27() real ext-real Element of REAL
dist ((lim G),(G . s)) is V27() real ext-real Element of REAL
the distance of X . ((lim G),(G . s)) is V27() real ext-real Element of REAL
(dist ((lim G),(G . s))) + (dist ((G . s),(G . Ht))) is V27() real ext-real Element of REAL
dist ((lim G),(G . Ht)) is V27() real ext-real Element of REAL
the distance of X . ((lim G),(G . Ht)) is V27() real ext-real Element of REAL
Ball ((G . Ht),(Gt . Ht)) is Element of bool the carrier of X
Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Y . Ht is Element of bool the carrier of X
G . Ht is Element of the carrier of X
Gt . Ht is V27() real ext-real Element of REAL
Ball ((G . Ht),(Gt . Ht)) is Element of bool the carrier of X
(Ball ((G . Ht),(Gt . Ht))) /\ (Y . Ht) is Element of bool the carrier of X
Ht is set
dom Y is Element of bool NAT
H is set
Y . H is set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
f is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
Y is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
f is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
ft is Element of the carrier of X
x is Element of the carrier of X
Y . (ft,x) is V27() real ext-real Element of REAL
ft - x is Element of the carrier of X
- x is Element of the carrier of X
ft + (- x) is Element of the carrier of X
the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K239( the carrier of X, the addF of X,ft,(- x)) is Element of the carrier of X
||.(ft - x).|| is V27() real ext-real Element of REAL
f . (ft,x) is V27() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
the carrier of MetrStruct(# the carrier of X,(X) #) is set
the distance of MetrStruct(# the carrier of X,(X) #) is V10() V13([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):]) V14( REAL ) Function-like V46([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:]
[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):] is set
[:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is set
bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is non empty set
Y is Element of the carrier of X
(X) . (Y,Y) is V27() real ext-real Element of REAL
Y - Y is Element of the carrier of X
- Y is Element of the carrier of X
Y + (- Y) is Element of the carrier of X
the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K239( the carrier of X, the addF of X,Y,(- Y)) is Element of the carrier of X
||.(Y - Y).|| is V27() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
the carrier of MetrStruct(# the carrier of X,(X) #) is set
the distance of MetrStruct(# the carrier of X,(X) #) is V10() V13([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):]) V14( REAL ) Function-like V46([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:]
[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):] is set
[:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is set
bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is non empty set
Y is Element of the carrier of X
f is Element of the carrier of X
(X) . (Y,f) is V27() real ext-real Element of REAL
Y - f is Element of the carrier of X
- f is Element of the carrier of X
Y + (- f) is Element of the carrier of X
the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K239( the carrier of X, the addF of X,Y,(- f)) is Element of the carrier of X
||.(Y - f).|| is V27() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
the carrier of MetrStruct(# the carrier of X,(X) #) is set
the distance of MetrStruct(# the carrier of X,(X) #) is V10() V13([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):]) V14( REAL ) Function-like V46([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:]
[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):] is set
[:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is set
bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is non empty set
Y is Element of the carrier of X
f is Element of the carrier of X
(X) . (Y,f) is V27() real ext-real Element of REAL
Y - f is Element of the carrier of X
- f is Element of the carrier of X
Y + (- f) is Element of the carrier of X
the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K239( the carrier of X, the addF of X,Y,(- f)) is Element of the carrier of X
||.(Y - f).|| is V27() real ext-real Element of REAL
f - Y is Element of the carrier of X
- Y is Element of the carrier of X
f + (- Y) is Element of the carrier of X
K239( the carrier of X, the addF of X,f,(- Y)) is Element of the carrier of X
||.(f - Y).|| is V27() real ext-real Element of REAL
(X) . (f,Y) is V27() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
the carrier of MetrStruct(# the carrier of X,(X) #) is set
the distance of MetrStruct(# the carrier of X,(X) #) is V10() V13([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):]) V14( REAL ) Function-like V46([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:]
[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):] is set
[:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is set
bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is non empty set
Y is Element of the carrier of X
ft is Element of the carrier of X
Y - ft is Element of the carrier of X
- ft is Element of the carrier of X
Y + (- ft) is Element of the carrier of X
the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K239( the carrier of X, the addF of X,Y,(- ft)) is Element of the carrier of X
||.(Y - ft).|| is V27() real ext-real Element of REAL
f is Element of the carrier of X
Y - f is Element of the carrier of X
- f is Element of the carrier of X
Y + (- f) is Element of the carrier of X
K239( the carrier of X, the addF of X,Y,(- f)) is Element of the carrier of X
||.(Y - f).|| is V27() real ext-real Element of REAL
f - ft is Element of the carrier of X
f + (- ft) is Element of the carrier of X
K239( the carrier of X, the addF of X,f,(- ft)) is Element of the carrier of X
||.(f - ft).|| is V27() real ext-real Element of REAL
||.(Y - f).|| + ||.(f - ft).|| is V27() real ext-real Element of REAL
(X) . (f,ft) is V27() real ext-real Element of REAL
||.(Y - f).|| + ((X) . (f,ft)) is V27() real ext-real Element of REAL
(X) . (Y,f) is V27() real ext-real Element of REAL
((X) . (Y,f)) + ((X) . (f,ft)) is V27() real ext-real Element of REAL
(X) . (Y,ft) is V27() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
the carrier of MetrStruct(# the carrier of X,(X) #) is set
the distance of MetrStruct(# the carrier of X,(X) #) is V10() V13([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):]) V14( REAL ) Function-like V46([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:]
[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):] is set
[:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is set
bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is non empty set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
f is V27() real ext-real set
Ball (Y,f) is Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
{ b1 where b1 is Element of the carrier of (X) : not f <= dist (Y,b1) } is set
xt is set
x is Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : not f <= ||.(x - b1).|| } is set
G is Element of the carrier of X
x - G is Element of the carrier of X
- G is Element of the carrier of X
x + (- G) is Element of the carrier of X
the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K239( the carrier of X, the addF of X,x,(- G)) is Element of the carrier of X
||.(x - G).|| is V27() real ext-real Element of REAL
Gt is Element of the carrier of (X)
dist (Y,Gt) is V27() real ext-real Element of REAL
the distance of (X) is V10() V13([: the carrier of (X), the carrier of (X):]) V14( REAL ) Function-like V46([: the carrier of (X), the carrier of (X):], REAL ) Element of bool [:[: the carrier of (X), the carrier of (X):],REAL:]
[: the carrier of (X), the carrier of (X):] is non empty set
[:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set
bool [:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set
the distance of (X) . (Y,Gt) is V27() real ext-real Element of REAL
xt is set
G is Element of the carrier of (X)
dist (Y,G) is V27() real ext-real Element of REAL
the distance of (X) . (Y,G) is V27() real ext-real Element of REAL
Gt is Element of the carrier of X
x - Gt is Element of the carrier of X
- Gt is Element of the carrier of X
x + (- Gt) is Element of the carrier of X
K239( the carrier of X, the addF of X,x,(- Gt)) is Element of the carrier of X
||.(x - Gt).|| is V27() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
f is V27() real ext-real set
cl_Ball (Y,f) is Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
{ b1 where b1 is Element of the carrier of (X) : dist (Y,b1) <= f } is set
xt is set
ft is Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : ||.(ft - b1).|| <= f } is set
G is Element of the carrier of X
ft - G is Element of the carrier of X
- G is Element of the carrier of X
ft + (- G) is Element of the carrier of X
the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K239( the carrier of X, the addF of X,ft,(- G)) is Element of the carrier of X
||.(ft - G).|| is V27() real ext-real Element of REAL
Gt is Element of the carrier of (X)
dist (Y,Gt) is V27() real ext-real Element of REAL
the distance of (X) is V10() V13([: the carrier of (X), the carrier of (X):]) V14( REAL ) Function-like V46([: the carrier of (X), the carrier of (X):], REAL ) Element of bool [:[: the carrier of (X), the carrier of (X):],REAL:]
[: the carrier of (X), the carrier of (X):] is non empty set
[:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set
bool [:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set
the distance of (X) . (Y,Gt) is V27() real ext-real Element of REAL
xt is set
G is Element of the carrier of (X)
dist (Y,G) is V27() real ext-real Element of REAL
the distance of (X) . (Y,G) is V27() real ext-real Element of REAL
Gt is Element of the carrier of X
ft - Gt is Element of the carrier of X
- Gt is Element of the carrier of X
ft + (- Gt) is Element of the carrier of X
K239( the carrier of X, the addF of X,ft,(- Gt)) is Element of the carrier of X
||.(ft - Gt).|| is V27() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
Y is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
ft is Element of the carrier of X
x is Element of the carrier of (X)
xt is V27() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Gt is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Y . Ht is Element of the carrier of X
(Y . Ht) - ft is Element of the carrier of X
- ft is Element of the carrier of X
(Y . Ht) + (- ft) is Element of the carrier of X
the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K239( the carrier of X, the addF of X,(Y . Ht),(- ft)) is Element of the carrier of X
||.((Y . Ht) - ft).|| is V27() real ext-real Element of REAL
f . Ht is Element of the carrier of (X)
dist ((f . Ht),x) is V27() real ext-real Element of REAL
the distance of (X) is V10() V13([: the carrier of (X), the carrier of (X):]) V14( REAL ) Function-like V46([: the carrier of (X), the carrier of (X):], REAL ) Element of bool [:[: the carrier of (X), the carrier of (X):],REAL:]
[: the carrier of (X), the carrier of (X):] is non empty set
[:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set
bool [:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set
the distance of (X) . ((f . Ht),x) is V27() real ext-real Element of REAL
xt is V27() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Gt is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
f . Ht is Element of the carrier of (X)
dist ((f . Ht),x) is V27() real ext-real Element of REAL
the distance of (X) . ((f . Ht),x) is V27() real ext-real Element of REAL
Y . Ht is Element of the carrier of X
(Y . Ht) - ft is Element of the carrier of X
(Y . Ht) + (- ft) is Element of the carrier of X
K239( the carrier of X, the addF of X,(Y . Ht),(- ft)) is Element of the carrier of X
||.((Y . Ht) - ft).|| is V27() real ext-real Element of REAL
xt is V27() real ext-real Element of REAL
G is V27() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
Y is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
ft is Element of the carrier of X
x is Element of the carrier of (X)
ft is Element of the carrier of (X)
x is Element of the carrier of X
xt is V27() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
Y is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
lim Y is Element of the carrier of X
f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
lim f is Element of the carrier of (X)
x is V27() real ext-real Element of REAL
ft is Element of the carrier of (X)
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is Element of bool the carrier of (X)
f is Element of the carrier of (X)
ft is Element of the carrier of X
x is V27() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of X : not x <= ||.(ft - b1).|| } is set
xt is V27() real ext-real Element of REAL
Ball (f,xt) is Element of bool the carrier of (X)
G is Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : not xt <= ||.(G - b1).|| } is set
the topology of (X) is Element of bool (bool the carrier of (X))
bool (bool the carrier of (X)) is non empty set
f is Element of the carrier of X
ft is Element of the carrier of (X)
x is V27() real ext-real Element of REAL
Ball (ft,x) is Element of bool the carrier of (X)
xt is V27() real ext-real Element of REAL
Ball (ft,xt) is Element of bool the carrier of (X)
{ b1 where b1 is Element of the carrier of X : not xt <= ||.(f - b1).|| } is set
G is Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : not xt <= ||.(G - b1).|| } is set
f is Element of the carrier of X
ft is Element of the carrier of X
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
(X) is non empty TopSpace-like TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is Element of the carrier of X
f is V27() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of X : not f <= ||.(Y - b1).|| } is set
ft is Element of the carrier of (X)
Ball (ft,f) is Element of bool the carrier of (X)
x is Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : not f <= ||.(x - b1).|| } is set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
(X) is non empty TopSpace-like TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is Element of the carrier of X
f is V27() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of X : ||.(Y - b1).|| <= f } is set
ft is Element of the carrier of (X)
cl_Ball (ft,f) is Element of bool the carrier of (X)
x is Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : ||.(x - b1).|| <= f } is set
X is non empty TopSpace-like T_2 TopStruct
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
Y is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
ft is Element of the carrier of X
x is Element of the carrier of (X)
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
xt is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
G is Element of the carrier of (X)
Gt is V27() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
Y is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
ft is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
Y is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
lim Y is Element of the carrier of X
{(lim Y)} is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
Lim f is Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
lim f is Element of the carrier of (X)
ft is Element of the carrier of (X)
{ft} is non empty Element of bool the carrier of (X)
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
x is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
lim x is Element of the carrier of (X)
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is Element of bool the carrier of X
f is Element of bool the carrier of (X)
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
ft is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
rng ft is Element of bool the carrier of (X)
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
x is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
lim x is Element of the carrier of X
{(lim x)} is non empty Element of bool the carrier of X
Lim ft is Element of bool the carrier of (X)
ft is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
rng ft is Element of bool the carrier of X
x is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
Lim x is Element of bool the carrier of (X)
lim ft is Element of the carrier of X
{(lim ft)} is non empty Element of bool the carrier of X
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is Element of bool the carrier of X
f is Element of bool the carrier of (X)
Y ` is Element of bool the carrier of X
the carrier of X \ Y is set
f ` is Element of bool the carrier of (X)
the carrier of (X) \ f is set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
Y is V27() real ext-real Element of REAL
f is Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : not Y <= ||.(f - b1).|| } is set
{ b1 where b1 is Element of the carrier of X : not Y <= ||.(b1 - f).|| } is set
ft is set
x is Element of the carrier of X
x - f is Element of the carrier of X
- f is Element of the carrier of X
x + (- f) is Element of the carrier of X
the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K239( the carrier of X, the addF of X,x,(- f)) is Element of the carrier of X
||.(x - f).|| is V27() real ext-real Element of REAL
f - x is Element of the carrier of X
- x is Element of the carrier of X
f + (- x) is Element of the carrier of X
K239( the carrier of X, the addF of X,f,(- x)) is Element of the carrier of X
||.(f - x).|| is V27() real ext-real Element of REAL
ft is set
x is Element of the carrier of X
f - x is Element of the carrier of X
- x is Element of the carrier of X
f + (- x) is Element of the carrier of X
K239( the carrier of X, the addF of X,f,(- x)) is Element of the carrier of X
||.(f - x).|| is V27() real ext-real Element of REAL
x - f is Element of the carrier of X
x + (- f) is Element of the carrier of X
K239( the carrier of X, the addF of X,x,(- f)) is Element of the carrier of X
||.(x - f).|| is V27() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is Element of bool the carrier of X
f is Element of bool the carrier of (X)
ft is Element of the carrier of X
x is Element of the carrier of (X)
xt is V27() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of X : not xt <= ||.(b1 - ft).|| } is set
G is set
Gt is Element of the carrier of X
Gt - ft is Element of the carrier of X
- ft is Element of the carrier of X
Gt + (- ft) is Element of the carrier of X
the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K239( the carrier of X, the addF of X,Gt,(- ft)) is Element of the carrier of X
||.(Gt - ft).|| is V27() real ext-real Element of REAL
G is Element of bool the carrier of (X)
{ b1 where b1 is Element of the carrier of X : not xt <= ||.(ft - b1).|| } is set
ft - ft is Element of the carrier of X
- ft is Element of the carrier of X
ft + (- ft) is Element of the carrier of X
the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K239( the carrier of X, the addF of X,ft,(- ft)) is Element of the carrier of X
||.(ft - ft).|| is V27() real ext-real Element of REAL
xt is Element of bool the carrier of (X)
G is V27() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of X : not G <= ||.(ft - b1).|| } is set
{ b1 where b1 is Element of the carrier of X : not G <= ||.(b1 - ft).|| } is set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
Y is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
(Y) is non empty TopSpace-like sequential TopStruct
(Y) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(Y) is V10() V13([: the carrier of Y, the carrier of Y:]) V14( REAL ) Function-like V46([: the carrier of Y, the carrier of Y:], REAL ) Element of bool [:[: the carrier of Y, the carrier of Y:],REAL:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:],REAL:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:],REAL:] is non empty set
MetrStruct(# the carrier of Y,(Y) #) is strict MetrStruct
TopSpaceMetr (Y) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (Y) is non empty set
Family_open_set (Y) is Element of bool (bool the carrier of (Y))
bool the carrier of (Y) is non empty set
bool (bool the carrier of (Y)) is non empty set
TopStruct(# the carrier of (Y),(Family_open_set (Y)) #) is strict TopStruct
the carrier of (Y) is non empty set
[: the carrier of (X), the carrier of (Y):] is non empty set
bool [: the carrier of (X), the carrier of (Y):] is non empty set
f is V10() V13( the carrier of X) V14( the carrier of Y) Function-like Element of bool [: the carrier of X, the carrier of Y:]
ft is V10() V13( the carrier of (X)) V14( the carrier of (Y)) Function-like V46( the carrier of (X), the carrier of (Y)) Element of bool [: the carrier of (X), the carrier of (Y):]
x is Element of the carrier of X
xt is Element of the carrier of (X)
dom f is Element of bool the carrier of X
bool the carrier of X is non empty set
ft . xt is Element of the carrier of (Y)
f /. x is Element of the carrier of Y
bool the carrier of Y is non empty set
G is a_neighborhood of ft . xt
Gt is Element of bool the carrier of Y
Ht is Neighbourhood of x
f .: Ht is Element of bool the carrier of Y
H is a_neighborhood of xt
H is a_neighborhood of xt
ft .: H is Element of bool the carrier of (Y)
bool the carrier of (Y) is non empty set
G is Neighbourhood of f /. x
Gt is Element of bool the carrier of Y
Ht is a_neighborhood of xt
ft .: Ht is Element of bool the carrier of (Y)
H is Element of bool the carrier of X
H is Neighbourhood of x
s is Neighbourhood of x
f .: s is Element of bool the carrier of Y
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
Y is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
(Y) is non empty TopSpace-like sequential TopStruct
(Y) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(Y) is V10() V13([: the carrier of Y, the carrier of Y:]) V14( REAL ) Function-like V46([: the carrier of Y, the carrier of Y:], REAL ) Element of bool [:[: the carrier of Y, the carrier of Y:],REAL:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:],REAL:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:],REAL:] is non empty set
MetrStruct(# the carrier of Y,(Y) #) is strict MetrStruct
TopSpaceMetr (Y) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (Y) is non empty set
Family_open_set (Y) is Element of bool (bool the carrier of (Y))
bool the carrier of (Y) is non empty set
bool (bool the carrier of (Y)) is non empty set
TopStruct(# the carrier of (Y),(Family_open_set (Y)) #) is strict TopStruct
the carrier of (Y) is non empty set
[: the carrier of (X), the carrier of (Y):] is non empty set
bool [: the carrier of (X), the carrier of (Y):] is non empty set
f is V10() V13( the carrier of X) V14( the carrier of Y) Function-like Element of bool [: the carrier of X, the carrier of Y:]
ft is V10() V13( the carrier of (X)) V14( the carrier of (Y)) Function-like V46( the carrier of (X), the carrier of (Y)) Element of bool [: the carrier of (X), the carrier of (Y):]
f | the carrier of X is V10() V13( the carrier of X) V14( the carrier of Y) Function-like Element of bool [: the carrier of X, the carrier of Y:]
x is Element of the carrier of (X)
xt is Element of the carrier of X
x is Element of the carrier of X
xt is Element of the carrier of (X)
dom f is Element of bool the carrier of X
bool the carrier of X is non empty set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
0. X is V57(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
[: the carrier of X, the carrier of X:] is non empty set
the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
[:REAL, the carrier of X:] is non empty set
the Mult of X is V10() V13([:REAL, the carrier of X:]) V14( the carrier of X) Function-like V46([:REAL, the carrier of X:], the carrier of X) Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:[:REAL, the carrier of X:], the carrier of X:] is non empty set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the topology of (X) is Element of bool (bool the carrier of (X))
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
Y is Element of bool (bool the carrier of X)
RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #) is non empty strict RLTopStruct
the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #) is non empty set
0. RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #) is V57( RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #)) Element of the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #)
the ZeroF of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #) is Element of the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #)
[: the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #), the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):] is non empty set
the addF of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #) is V10() V13([: the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #), the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):]) V14( the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #)) Function-like V46([: the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #), the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):], the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #)) Element of bool [:[: the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #), the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):], the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):]
[:[: the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #), the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):], the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):] is non empty set
bool [:[: the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #), the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):], the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):] is non empty set
[:REAL, the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):] is non empty set
the Mult of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #) is V10() V13([:REAL, the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):]) V14( the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #)) Function-like V46([:REAL, the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):], the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #)) Element of bool [:[:REAL, the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):], the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):]
[:[:REAL, the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):], the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):] is non empty set
bool [:[:REAL, the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):], the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #):] is non empty set
the topology of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #) is Element of bool (bool the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #))
bool the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #) is non empty set
bool (bool the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,Y #)) is non empty set
Y is non empty strict RLTopStruct
the carrier of Y is non empty set
0. Y is V57(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
[: the carrier of Y, the carrier of Y:] is non empty set
the addF of Y is V10() V13([: the carrier of Y, the carrier of Y:]) V14( the carrier of Y) Function-like V46([: the carrier of Y, the carrier of Y:], the carrier of Y) Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
[:REAL, the carrier of Y:] is non empty set
the Mult of Y is V10() V13([:REAL, the carrier of Y:]) V14( the carrier of Y) Function-like V46([:REAL, the carrier of Y:], the carrier of Y) Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
the topology of Y is Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
f is non empty strict RLTopStruct
the carrier of f is non empty set
0. f is V57(f) Element of the carrier of f
the ZeroF of f is Element of the carrier of f
[: the carrier of f, the carrier of f:] is non empty set
the addF of f is V10() V13([: the carrier of f, the carrier of f:]) V14( the carrier of f) Function-like V46([: the carrier of f, the carrier of f:], the carrier of f) Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
[:REAL, the carrier of f:] is non empty set
the Mult of f is V10() V13([:REAL, the carrier of f:]) V14( the carrier of f) Function-like V46([:REAL, the carrier of f:], the carrier of f) Element of bool [:[:REAL, the carrier of f:], the carrier of f:]
[:[:REAL, the carrier of f:], the carrier of f:] is non empty set
bool [:[:REAL, the carrier of f:], the carrier of f:] is non empty set
the topology of f is Element of bool (bool the carrier of f)
bool the carrier of f is non empty set
bool (bool the carrier of f) is non empty set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty strict RLTopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is Element of the carrier of (X)
f is Element of the carrier of (X)
Y + f is Element of the carrier of (X)
the addF of (X) is V10() V13([: the carrier of (X), the carrier of (X):]) V14( the carrier of (X)) Function-like V46([: the carrier of (X), the carrier of (X):], the carrier of (X)) Element of bool [:[: the carrier of (X), the carrier of (X):], the carrier of (X):]
[: the carrier of (X), the carrier of (X):] is non empty set
[:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set
bool [:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set
K239( the carrier of (X), the addF of (X),Y,f) is Element of the carrier of (X)
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
the carrier of (X) is non empty set
G is Element of bool the carrier of (X)
the topology of (X) is Element of bool (bool the carrier of (X))
bool (bool the carrier of (X)) is non empty set
(X) is non empty TopSpace-like sequential TopStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the topology of (X) is Element of bool (bool the carrier of (X))
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
xt is Element of the carrier of (X)
Gt is V27() real ext-real Element of REAL
Ball (xt,Gt) is Element of bool the carrier of (X)
Gt / 2 is V27() real ext-real Element of REAL
x is Element of the carrier of (X)
Ball (x,(Gt / 2)) is Element of bool the carrier of (X)
ft is Element of the carrier of (X)
Ball (ft,(Gt / 2)) is Element of bool the carrier of (X)
H is Element of bool the carrier of (X)
H is Element of bool the carrier of (X)
H + H is Element of bool the carrier of (X)
{ (b1 + b2) where b1, b2 is Element of the carrier of (X) : ( b1 in H & b2 in H ) } is set
s is set
w is Element of the carrier of (X)
v is Element of the carrier of (X)
w + v is Element of the carrier of (X)
K239( the carrier of (X), the addF of (X),w,v) is Element of the carrier of (X)
vv1 is Element of the carrier of X
vv1 is Element of the carrier of X
vv1 - vv1 is Element of the carrier of X
- vv1 is Element of the carrier of X
vv1 + (- vv1) is Element of the carrier of X
the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K239( the carrier of X, the addF of X,vv1,(- vv1)) is Element of the carrier of X
ww1 is Element of the carrier of X
uu1 is Element of the carrier of X
ww1 - uu1 is Element of the carrier of X
- uu1 is Element of the carrier of X
ww1 + (- uu1) is Element of the carrier of X
K239( the carrier of X, the addF of X,ww1,(- uu1)) is Element of the carrier of X
(vv1 - vv1) + (ww1 - uu1) is Element of the carrier of X
K239( the carrier of X, the addF of X,(vv1 - vv1),(ww1 - uu1)) is Element of the carrier of X
||.((vv1 - vv1) + (ww1 - uu1)).|| is V27() real ext-real Element of REAL
||.(vv1 - vv1).|| is V27() real ext-real Element of REAL
||.(ww1 - uu1).|| is V27() real ext-real Element of REAL
||.(vv1 - vv1).|| + ||.(ww1 - uu1).|| is V27() real ext-real Element of REAL
v1 is Element of the carrier of (X)
dist (x,v1) is V27() real ext-real Element of REAL
the distance of (X) is V10() V13([: the carrier of (X), the carrier of (X):]) V14( REAL ) Function-like V46([: the carrier of (X), the carrier of (X):], REAL ) Element of bool [:[: the carrier of (X), the carrier of (X):],REAL:]
[: the carrier of (X), the carrier of (X):] is non empty set
[:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set
bool [:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set
the distance of (X) . (x,v1) is V27() real ext-real Element of REAL
w1 is Element of the carrier of (X)
dist (ft,w1) is V27() real ext-real Element of REAL
the distance of (X) . (ft,w1) is V27() real ext-real Element of REAL
(Gt / 2) + (Gt / 2) is V27() real ext-real Element of REAL
(dist (x,v1)) + (dist (ft,w1)) is V27() real ext-real Element of REAL
zza is Element of the carrier of (X)
dist (xt,zza) is V27() real ext-real Element of REAL
the distance of (X) . (xt,zza) is V27() real ext-real Element of REAL
zz is Element of the carrier of X
ww1 is Element of the carrier of X
zz - ww1 is Element of the carrier of X
- ww1 is Element of the carrier of X
zz + (- ww1) is Element of the carrier of X
K239( the carrier of X, the addF of X,zz,(- ww1)) is Element of the carrier of X
||.(zz - ww1).|| is V27() real ext-real Element of REAL
vv1 + ww1 is Element of the carrier of X
K239( the carrier of X, the addF of X,vv1,ww1) is Element of the carrier of X
(vv1 + ww1) - ww1 is Element of the carrier of X
(vv1 + ww1) + (- ww1) is Element of the carrier of X
K239( the carrier of X, the addF of X,(vv1 + ww1),(- ww1)) is Element of the carrier of X
||.((vv1 + ww1) - ww1).|| is V27() real ext-real Element of REAL
vv1 + uu1 is Element of the carrier of X
K239( the carrier of X, the addF of X,vv1,uu1) is Element of the carrier of X
(vv1 + ww1) - (vv1 + uu1) is Element of the carrier of X
- (vv1 + uu1) is Element of the carrier of X
(vv1 + ww1) + (- (vv1 + uu1)) is Element of the carrier of X
K239( the carrier of X, the addF of X,(vv1 + ww1),(- (vv1 + uu1))) is Element of the carrier of X
||.((vv1 + ww1) - (vv1 + uu1)).|| is V27() real ext-real Element of REAL
(- uu1) + (- vv1) is Element of the carrier of X
K239( the carrier of X, the addF of X,(- uu1),(- vv1)) is Element of the carrier of X
(vv1 + ww1) + ((- uu1) + (- vv1)) is Element of the carrier of X
K239( the carrier of X, the addF of X,(vv1 + ww1),((- uu1) + (- vv1))) is Element of the carrier of X
||.((vv1 + ww1) + ((- uu1) + (- vv1))).|| is V27() real ext-real Element of REAL
(vv1 + ww1) + (- vv1) is Element of the carrier of X
K239( the carrier of X, the addF of X,(vv1 + ww1),(- vv1)) is Element of the carrier of X
((vv1 + ww1) + (- vv1)) + (- uu1) is Element of the carrier of X
K239( the carrier of X, the addF of X,((vv1 + ww1) + (- vv1)),(- uu1)) is Element of the carrier of X
||.(((vv1 + ww1) + (- vv1)) + (- uu1)).|| is V27() real ext-real Element of REAL
vv1 + (- vv1) is Element of the carrier of X
(vv1 + (- vv1)) + ww1 is Element of the carrier of X
K239( the carrier of X, the addF of X,(vv1 + (- vv1)),ww1) is Element of the carrier of X
((vv1 + (- vv1)) + ww1) + (- uu1) is Element of the carrier of X
K239( the carrier of X, the addF of X,((vv1 + (- vv1)) + ww1),(- uu1)) is Element of the carrier of X
||.(((vv1 + (- vv1)) + ww1) + (- uu1)).|| is V27() real ext-real Element of REAL
ww1 + (- uu1) is Element of the carrier of X
(vv1 + (- vv1)) + (ww1 + (- uu1)) is Element of the carrier of X
K239( the carrier of X, the addF of X,(vv1 + (- vv1)),(ww1 + (- uu1))) is Element of the carrier of X
||.((vv1 + (- vv1)) + (ww1 + (- uu1))).|| is V27() real ext-real Element of REAL
dist (ft,ft) is V27() real ext-real Element of REAL
the distance of (X) is V10() V13([: the carrier of (X), the carrier of (X):]) V14( REAL ) Function-like V46([: the carrier of (X), the carrier of (X):], REAL ) Element of bool [:[: the carrier of (X), the carrier of (X):],REAL:]
[: the carrier of (X), the carrier of (X):] is non empty set
[:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set
bool [:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set
the distance of (X) . (ft,ft) is V27() real ext-real Element of REAL
dist (x,x) is V27() real ext-real Element of REAL
the distance of (X) . (x,x) is V27() real ext-real Element of REAL
the carrier of (X) is non empty set
the carrier of X is non empty set
ft is Element of the carrier of (X)
Y is V27() real ext-real set
Y * ft is Element of the carrier of (X)
the Mult of (X) is V10() V13([:REAL, the carrier of (X):]) V14( the carrier of (X)) Function-like V46([:REAL, the carrier of (X):], the carrier of (X)) Element of bool [:[:REAL, the carrier of (X):], the carrier of (X):]
[:REAL, the carrier of (X):] is non empty set
[:[:REAL, the carrier of (X):], the carrier of (X):] is non empty set
bool [:[:REAL, the carrier of (X):], the carrier of (X):] is non empty set
K235( the Mult of (X),Y,ft) is set
x is Element of the carrier of X
Y * x is Element of the carrier of X
the Mult of X is V10() V13([:REAL, the carrier of X:]) V14( the carrier of X) Function-like V46([:REAL, the carrier of X:], the carrier of X) Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K235( the Mult of X,Y,x) is set
f is V27() real ext-real set
f * ft is Element of the carrier of (X)
K235( the Mult of (X),f,ft) is set
f * x is Element of the carrier of X
K235( the Mult of X,f,x) is set
(Y * x) + (f * x) is Element of the carrier of X
the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K239( the carrier of X, the addF of X,(Y * x),(f * x)) is Element of the carrier of X
(Y * ft) + (f * ft) is Element of the carrier of (X)
the addF of (X) is V10() V13([: the carrier of (X), the carrier of (X):]) V14( the carrier of (X)) Function-like V46([: the carrier of (X), the carrier of (X):], the carrier of (X)) Element of bool [:[: the carrier of (X), the carrier of (X):], the carrier of (X):]
[: the carrier of (X), the carrier of (X):] is non empty set
[:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set
bool [:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set
K239( the carrier of (X), the addF of (X),(Y * ft),(f * ft)) is Element of the carrier of (X)
Y + f is V27() real ext-real set
(Y + f) * ft is Element of the carrier of (X)
K235( the Mult of (X),(Y + f),ft) is set
(Y + f) * x is Element of the carrier of X
K235( the Mult of X,(Y + f),x) is set
bool the carrier of (X) is non empty set
Y is V27() real ext-real Element of REAL
f is Element of the carrier of (X)
Y * f is Element of the carrier of (X)
K235( the Mult of (X),Y,f) is set
ft is Element of bool the carrier of (X)
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
the carrier of (X) is non empty set
the topology of (X) is Element of bool (bool the carrier of (X))
bool (bool the carrier of (X)) is non empty set
(X) is non empty TopSpace-like sequential TopStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the topology of (X) is Element of bool (bool the carrier of (X))
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
xt is Element of the carrier of (X)
G is V27() real ext-real Element of REAL
Ball (xt,G) is Element of bool the carrier of (X)
G / 2 is V27() real ext-real Element of REAL
(G / 2) / 2 is V27() real ext-real Element of REAL
x is Element of the carrier of (X)
Ht is Element of the carrier of X
||.Ht.|| is V27() real ext-real Element of REAL
1 + ||.Ht.|| is V27() real ext-real Element of REAL
abs Y is V27() real ext-real Element of REAL
(1 + ||.Ht.||) + (abs Y) is V27() real ext-real Element of REAL
((G / 2) / 2) / ((1 + ||.Ht.||) + (abs Y)) is V27() real ext-real Element of REAL
min ((((G / 2) / 2) / ((1 + ||.Ht.||) + (abs Y))),1) is V27() real ext-real Element of REAL
Ball (x,(min ((((G / 2) / 2) / ((1 + ||.Ht.||) + (abs Y))),1))) is Element of bool the carrier of (X)
G / 1 is V27() real ext-real Element of REAL
H is Element of bool the carrier of (X)
s is V27() real ext-real Element of REAL
s - Y is V27() real ext-real Element of REAL
abs (s - Y) is V27() real ext-real Element of REAL
s * H is Element of bool the carrier of (X)
{ (s * b1) where b1 is Element of the carrier of (X) : b1 in H } is set
Y - s is V27() real ext-real Element of REAL
abs (Y - s) is V27() real ext-real Element of REAL
w is set
v is Element of the carrier of (X)
s * v is Element of the carrier of (X)
K235( the Mult of (X),s,v) is set
v1 is Element of the carrier of (X)
dist (x,v1) is V27() real ext-real Element of REAL
the distance of (X) is V10() V13([: the carrier of (X), the carrier of (X):]) V14( REAL ) Function-like V46([: the carrier of (X), the carrier of (X):], REAL ) Element of bool [:[: the carrier of (X), the carrier of (X):],REAL:]
[: the carrier of (X), the carrier of (X):] is non empty set
[:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set
bool [:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set
the distance of (X) . (x,v1) is V27() real ext-real Element of REAL
zz is Element of the carrier of X
vv1 is Element of the carrier of X
zz - vv1 is Element of the carrier of X
- vv1 is Element of the carrier of X
zz + (- vv1) is Element of the carrier of X
K239( the carrier of X, the addF of X,zz,(- vv1)) is Element of the carrier of X
||.(zz - vv1).|| is V27() real ext-real Element of REAL
vv1 - zz is Element of the carrier of X
- zz is Element of the carrier of X
vv1 + (- zz) is Element of the carrier of X
K239( the carrier of X, the addF of X,vv1,(- zz)) is Element of the carrier of X
||.(vv1 - zz).|| is V27() real ext-real Element of REAL
||.zz.|| is V27() real ext-real Element of REAL
||.zz.|| + ||.(vv1 - zz).|| is V27() real ext-real Element of REAL
||.zz.|| + 1 is V27() real ext-real Element of REAL
zz + (vv1 - zz) is Element of the carrier of X
K239( the carrier of X, the addF of X,zz,(vv1 - zz)) is Element of the carrier of X
zz - zz is Element of the carrier of X
zz + (- zz) is Element of the carrier of X
K239( the carrier of X, the addF of X,zz,(- zz)) is Element of the carrier of X
vv1 - (zz - zz) is Element of the carrier of X
- (zz - zz) is Element of the carrier of X
vv1 + (- (zz - zz)) is Element of the carrier of X
K239( the carrier of X, the addF of X,vv1,(- (zz - zz))) is Element of the carrier of X
0. X is V57(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
vv1 - (0. X) is Element of the carrier of X
- (0. X) is Element of the carrier of X
vv1 + (- (0. X)) is Element of the carrier of X
K239( the carrier of X, the addF of X,vv1,(- (0. X))) is Element of the carrier of X
||.vv1.|| is V27() real ext-real Element of REAL
(min ((((G / 2) / 2) / ((1 + ||.Ht.||) + (abs Y))),1)) * (||.zz.|| + 1) is V27() real ext-real Element of REAL
(((G / 2) / 2) / ((1 + ||.Ht.||) + (abs Y))) * (||.zz.|| + 1) is V27() real ext-real Element of REAL
(abs (Y - s)) * ||.vv1.|| is V27() real ext-real Element of REAL
||.Ht.|| + 1 is V27() real ext-real Element of REAL
(((G / 2) / 2) / ((1 + ||.Ht.||) + (abs Y))) * (||.Ht.|| + 1) is V27() real ext-real Element of REAL
(||.Ht.|| + 1) / ((1 + ||.Ht.||) + (abs Y)) is V27() real ext-real Element of REAL
((||.Ht.|| + 1) / ((1 + ||.Ht.||) + (abs Y))) * ((G / 2) / 2) is V27() real ext-real Element of REAL
0 + (1 + ||.Ht.||) is V27() real ext-real Element of REAL
(abs Y) + (1 + ||.Ht.||) is V27() real ext-real Element of REAL
1 * ((G / 2) / 2) is V27() real ext-real Element of REAL
Y * (zz - vv1) is Element of the carrier of X
K235( the Mult of X,Y,(zz - vv1)) is set
(s - Y) * vv1 is Element of the carrier of X
K235( the Mult of X,(s - Y),vv1) is set
(Y * (zz - vv1)) - ((s - Y) * vv1) is Element of the carrier of X
- ((s - Y) * vv1) is Element of the carrier of X
(Y * (zz - vv1)) + (- ((s - Y) * vv1)) is Element of the carrier of X
K239( the carrier of X, the addF of X,(Y * (zz - vv1)),(- ((s - Y) * vv1))) is Element of the carrier of X
Y * zz is Element of the carrier of X
K235( the Mult of X,Y,zz) is set
Y * vv1 is Element of the carrier of X
K235( the Mult of X,Y,vv1) is set
(Y * zz) - (Y * vv1) is Element of the carrier of X
- (Y * vv1) is Element of the carrier of X
(Y * zz) + (- (Y * vv1)) is Element of the carrier of X
K239( the carrier of X, the addF of X,(Y * zz),(- (Y * vv1))) is Element of the carrier of X
((Y * zz) - (Y * vv1)) - ((s - Y) * vv1) is Element of the carrier of X
((Y * zz) - (Y * vv1)) + (- ((s - Y) * vv1)) is Element of the carrier of X
K239( the carrier of X, the addF of X,((Y * zz) - (Y * vv1)),(- ((s - Y) * vv1))) is Element of the carrier of X
s * vv1 is Element of the carrier of X
K235( the Mult of X,s,vv1) is set
(s * vv1) - (Y * vv1) is Element of the carrier of X
(s * vv1) + (- (Y * vv1)) is Element of the carrier of X
K239( the carrier of X, the addF of X,(s * vv1),(- (Y * vv1))) is Element of the carrier of X
((Y * zz) - (Y * vv1)) - ((s * vv1) - (Y * vv1)) is Element of the carrier of X
- ((s * vv1) - (Y * vv1)) is Element of the carrier of X
((Y * zz) - (Y * vv1)) + (- ((s * vv1) - (Y * vv1))) is Element of the carrier of X
K239( the carrier of X, the addF of X,((Y * zz) - (Y * vv1)),(- ((s * vv1) - (Y * vv1)))) is Element of the carrier of X
((s * vv1) - (Y * vv1)) + (Y * vv1) is Element of the carrier of X
K239( the carrier of X, the addF of X,((s * vv1) - (Y * vv1)),(Y * vv1)) is Element of the carrier of X
(Y * zz) - (((s * vv1) - (Y * vv1)) + (Y * vv1)) is Element of the carrier of X
- (((s * vv1) - (Y * vv1)) + (Y * vv1)) is Element of the carrier of X
(Y * zz) + (- (((s * vv1) - (Y * vv1)) + (Y * vv1))) is Element of the carrier of X
K239( the carrier of X, the addF of X,(Y * zz),(- (((s * vv1) - (Y * vv1)) + (Y * vv1)))) is Element of the carrier of X
(Y * vv1) - (Y * vv1) is Element of the carrier of X
(Y * vv1) + (- (Y * vv1)) is Element of the carrier of X
K239( the carrier of X, the addF of X,(Y * vv1),(- (Y * vv1))) is Element of the carrier of X
(s * vv1) - ((Y * vv1) - (Y * vv1)) is Element of the carrier of X
- ((Y * vv1) - (Y * vv1)) is Element of the carrier of X
(s * vv1) + (- ((Y * vv1) - (Y * vv1))) is Element of the carrier of X
K239( the carrier of X, the addF of X,(s * vv1),(- ((Y * vv1) - (Y * vv1)))) is Element of the carrier of X
(Y * zz) - ((s * vv1) - ((Y * vv1) - (Y * vv1))) is Element of the carrier of X
- ((s * vv1) - ((Y * vv1) - (Y * vv1))) is Element of the carrier of X
(Y * zz) + (- ((s * vv1) - ((Y * vv1) - (Y * vv1)))) is Element of the carrier of X
K239( the carrier of X, the addF of X,(Y * zz),(- ((s * vv1) - ((Y * vv1) - (Y * vv1))))) is Element of the carrier of X
(s * vv1) - (0. X) is Element of the carrier of X
(s * vv1) + (- (0. X)) is Element of the carrier of X
K239( the carrier of X, the addF of X,(s * vv1),(- (0. X))) is Element of the carrier of X
(Y * zz) - ((s * vv1) - (0. X)) is Element of the carrier of X
- ((s * vv1) - (0. X)) is Element of the carrier of X
(Y * zz) + (- ((s * vv1) - (0. X))) is Element of the carrier of X
K239( the carrier of X, the addF of X,(Y * zz),(- ((s * vv1) - (0. X)))) is Element of the carrier of X
(Y * zz) - (s * vv1) is Element of the carrier of X
- (s * vv1) is Element of the carrier of X
(Y * zz) + (- (s * vv1)) is Element of the carrier of X
K239( the carrier of X, the addF of X,(Y * zz),(- (s * vv1))) is Element of the carrier of X
||.((Y * zz) - (s * vv1)).|| is V27() real ext-real Element of REAL
||.(Y * (zz - vv1)).|| is V27() real ext-real Element of REAL
||.((s - Y) * vv1).|| is V27() real ext-real Element of REAL
||.(Y * (zz - vv1)).|| + ||.((s - Y) * vv1).|| is V27() real ext-real Element of REAL
(abs Y) * ||.(zz - vv1).|| is V27() real ext-real Element of REAL
((abs Y) * ||.(zz - vv1).||) + ||.((s - Y) * vv1).|| is V27() real ext-real Element of REAL
(abs (s - Y)) * ||.vv1.|| is V27() real ext-real Element of REAL
((abs Y) * ||.(zz - vv1).||) + ((abs (s - Y)) * ||.vv1.||) is V27() real ext-real Element of REAL
((abs Y) * ||.(zz - vv1).||) + ((abs (Y - s)) * ||.vv1.||) is V27() real ext-real Element of REAL
(min ((((G / 2) / 2) / ((1 + ||.Ht.||) + (abs Y))),1)) * (abs Y) is V27() real ext-real Element of REAL
(((G / 2) / 2) / ((1 + ||.Ht.||) + (abs Y))) * (abs Y) is V27() real ext-real Element of REAL
0 + (abs Y) is V27() real ext-real Element of REAL
(abs Y) / ((1 + ||.Ht.||) + (abs Y)) is V27() real ext-real Element of REAL
((abs Y) / ((1 + ||.Ht.||) + (abs Y))) * ((G / 2) / 2) is V27() real ext-real Element of REAL
||.(zz - vv1).|| * (abs Y) is V27() real ext-real Element of REAL
(abs Y) * (((G / 2) / 2) / ((1 + ||.Ht.||) + (abs Y))) is V27() real ext-real Element of REAL
((G / 2) / 2) + ((G / 2) / 2) is V27() real ext-real Element of REAL
w1 is Element of the carrier of (X)
dist (xt,w1) is V27() real ext-real Element of REAL
the distance of (X) . (xt,w1) is V27() real ext-real Element of REAL
zza is Element of the carrier of X
ww1 is Element of the carrier of X
zza - ww1 is Element of the carrier of X
- ww1 is Element of the carrier of X
zza + (- ww1) is Element of the carrier of X
K239( the carrier of X, the addF of X,zza,(- ww1)) is Element of the carrier of X
||.(zza - ww1).|| is V27() real ext-real Element of REAL
(Y * zz) - ww1 is Element of the carrier of X
(Y * zz) + (- ww1) is Element of the carrier of X
K239( the carrier of X, the addF of X,(Y * zz),(- ww1)) is Element of the carrier of X
||.((Y * zz) - ww1).|| is V27() real ext-real Element of REAL
0 / ((1 + ||.Ht.||) + (abs Y)) is V27() real ext-real Element of REAL
dist (x,x) is V27() real ext-real Element of REAL
the distance of (X) is V10() V13([: the carrier of (X), the carrier of (X):]) V14( REAL ) Function-like V46([: the carrier of (X), the carrier of (X):], REAL ) Element of bool [:[: the carrier of (X), the carrier of (X):],REAL:]
[: the carrier of (X), the carrier of (X):] is non empty set
[:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set
bool [:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set
the distance of (X) . (x,x) is V27() real ext-real Element of REAL
the topology of (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the topology of (X) is Element of bool (bool the carrier of (X))
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
f is Element of bool the carrier of (X)
ft is Element of bool the carrier of (X)
f /\ ft is Element of bool the carrier of (X)
f is Element of bool (bool the carrier of (X))
union f is Element of bool the carrier of (X)
Y is Element of the carrier of (X)
f is Element of the carrier of (X)
Y + f is Element of the carrier of (X)
K239( the carrier of (X), the addF of (X),Y,f) is Element of the carrier of (X)
f + Y is Element of the carrier of (X)
K239( the carrier of (X), the addF of (X),f,Y) is Element of the carrier of (X)
ft is Element of the carrier of X
x is Element of the carrier of X
ft + x is Element of the carrier of X
K239( the carrier of X, the addF of X,ft,x) is Element of the carrier of X
x + ft is Element of the carrier of X
K239( the carrier of X, the addF of X,x,ft) is Element of the carrier of X
Y is Element of the carrier of (X)
f is Element of the carrier of (X)
Y + f is Element of the carrier of (X)
K239( the carrier of (X), the addF of (X),Y,f) is Element of the carrier of (X)
ft is Element of the carrier of (X)
(Y + f) + ft is Element of the carrier of (X)
K239( the carrier of (X), the addF of (X),(Y + f),ft) is Element of the carrier of (X)
f + ft is Element of the carrier of (X)
K239( the carrier of (X), the addF of (X),f,ft) is Element of the carrier of (X)
Y + (f + ft) is Element of the carrier of (X)
K239( the carrier of (X), the addF of (X),Y,(f + ft)) is Element of the carrier of (X)
xt is Element of the carrier of X
G is Element of the carrier of X
xt + G is Element of the carrier of X
K239( the carrier of X, the addF of X,xt,G) is Element of the carrier of X
x is Element of the carrier of X
x + xt is Element of the carrier of X
K239( the carrier of X, the addF of X,x,xt) is Element of the carrier of X
(x + xt) + G is Element of the carrier of X
K239( the carrier of X, the addF of X,(x + xt),G) is Element of the carrier of X
x + (xt + G) is Element of the carrier of X
K239( the carrier of X, the addF of X,x,(xt + G)) is Element of the carrier of X
Y is Element of the carrier of (X)
0. (X) is V57((X)) Element of the carrier of (X)
the ZeroF of (X) is Element of the carrier of (X)
Y + (0. (X)) is Element of the carrier of (X)
K239( the carrier of (X), the addF of (X),Y,(0. (X))) is Element of the carrier of (X)
0. X is V57(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
f is Element of the carrier of X
f + (0. X) is Element of the carrier of X
K239( the carrier of X, the addF of X,f,(0. X)) is Element of the carrier of X
Y is Element of the carrier of (X)
f is Element of the carrier of X
- f is Element of the carrier of X
ft is Element of the carrier of (X)
Y + ft is Element of the carrier of (X)
K239( the carrier of (X), the addF of (X),Y,ft) is Element of the carrier of (X)
0. (X) is V57((X)) Element of the carrier of (X)
the ZeroF of (X) is Element of the carrier of (X)
f - f is Element of the carrier of X
f + (- f) is Element of the carrier of X
K239( the carrier of X, the addF of X,f,(- f)) is Element of the carrier of X
0. X is V57(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
ft is Element of the carrier of (X)
f is V27() real ext-real set
f * ft is Element of the carrier of (X)
K235( the Mult of (X),f,ft) is set
x is Element of the carrier of X
f * x is Element of the carrier of X
K235( the Mult of X,f,x) is set
Y is V27() real ext-real set
Y * (f * x) is Element of the carrier of X
K235( the Mult of X,Y,(f * x)) is set
Y * (f * ft) is Element of the carrier of (X)
K235( the Mult of (X),Y,(f * ft)) is set
Y * f is V27() real ext-real set
(Y * f) * x is Element of the carrier of X
K235( the Mult of X,(Y * f),x) is set
(Y * f) * ft is Element of the carrier of (X)
K235( the Mult of (X),(Y * f),ft) is set
f is Element of the carrier of (X)
ft is Element of the carrier of (X)
Y is V27() real ext-real set
Y * f is Element of the carrier of (X)
K235( the Mult of (X),Y,f) is set
x is Element of the carrier of X
Y * x is Element of the carrier of X
K235( the Mult of X,Y,x) is set
Y * ft is Element of the carrier of (X)
K235( the Mult of (X),Y,ft) is set
xt is Element of the carrier of X
Y * xt is Element of the carrier of X
K235( the Mult of X,Y,xt) is set
(Y * x) + (Y * xt) is Element of the carrier of X
K239( the carrier of X, the addF of X,(Y * x),(Y * xt)) is Element of the carrier of X
(Y * f) + (Y * ft) is Element of the carrier of (X)
K239( the carrier of (X), the addF of (X),(Y * f),(Y * ft)) is Element of the carrier of (X)
f + ft is Element of the carrier of (X)
K239( the carrier of (X), the addF of (X),f,ft) is Element of the carrier of (X)
x + xt is Element of the carrier of X
K239( the carrier of X, the addF of X,x,xt) is Element of the carrier of X
Y * (f + ft) is Element of the carrier of (X)
K235( the Mult of (X),Y,(f + ft)) is set
Y * (x + xt) is Element of the carrier of X
K235( the Mult of X,Y,(x + xt)) is set
Y is Element of the carrier of (X)
1 * Y is Element of the carrier of (X)
K235( the Mult of (X),1,Y) is set
f is Element of the carrier of X
1 * f is Element of the carrier of X
K235( the Mult of X,1,f) is set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
(X) is non empty TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is Element of bool the carrier of (X)
f is Element of bool the carrier of (X)
the topology of (X) is Element of bool (bool the carrier of (X))
bool (bool the carrier of (X)) is non empty set
the topology of (X) is Element of bool (bool the carrier of (X))
bool (bool the carrier of (X)) is non empty set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
(X) is non empty TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is Element of bool the carrier of (X)
f is Element of bool the carrier of (X)
f ` is Element of bool the carrier of (X)
the carrier of (X) \ f is set
Y ` is Element of bool the carrier of (X)
the carrier of (X) \ Y is set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
the carrier of X is non empty set
Y is Element of bool the carrier of (X)
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
f is Element of bool the carrier of (X)
ft is Element of the carrier of X
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
(X) is non empty TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is Element of the carrier of X
f is V27() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of X : not f <= ||.(Y - b1).|| } is set
ft is Element of bool the carrier of (X)
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
x is Element of bool the carrier of (X)
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is Element of the carrier of X
f is V27() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of X : ||.(Y - b1).|| <= f } is set
ft is Element of bool the carrier of (X)
x is Element of the carrier of (X)
cl_Ball (x,f) is Element of bool the carrier of (X)
xt is Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : ||.(xt - b1).|| <= f } is set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
f is Element of the carrier of (X)
bool the carrier of (X) is non empty set
the topology of (X) is Element of bool (bool the carrier of (X))
bool (bool the carrier of (X)) is non empty set
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the topology of (X) is Element of bool (bool the carrier of (X))
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
ft is Element of the carrier of (X)
x is Element of the carrier of (X)
xt is Element of bool the carrier of (X)
G is Element of bool the carrier of (X)
Ht is Element of bool the carrier of (X)
Gt is Element of bool the carrier of (X)
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
(X) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
Y is Element of bool (bool the carrier of (X))
f is Element of bool (bool the carrier of (X))
ft is Element of the carrier of (X)
x is Element of the carrier of (X)
Intersect Y is Element of bool the carrier of (X)
Intersect f is Element of bool the carrier of (X)
the topology of (X) is Element of bool (bool the carrier of (X))
the topology of (X) is Element of bool (bool the carrier of (X))
xt is Element of bool the carrier of (X)
G is open Element of bool the carrier of (X)
Gt is Element of bool the carrier of (X)
Ht is Element of bool the carrier of (X)
H is Element of bool the carrier of (X)
xt is Element of bool the carrier of (X)
G is open Element of bool the carrier of (X)
Gt is Element of bool the carrier of (X)
Ht is Element of bool the carrier of (X)
H is Element of bool the carrier of (X)
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
f is Element of the carrier of (X)
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
ft is non empty f -quasi_basis V251((X)) Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
x is non empty Y -quasi_basis V251((X)) Element of bool (bool the carrier of (X))
xt is non empty Y -quasi_basis V251((X)) Element of bool (bool the carrier of (X))
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
(X) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober first-countable Frechet sequential strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
Y is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
ft is Element of the carrier of (X)
x is Element of the carrier of (X)
bool the carrier of (X) is non empty set
xt is Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
G is open Element of bool the carrier of (X)
Gt is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
f . H is Element of the carrier of (X)
xt is Element of bool the carrier of (X)
G is open Element of bool the carrier of (X)
Gt is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT
Y . H is Element of the carrier of (X)
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
(X) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober first-countable Frechet sequential strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
Y is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
ft is Element of the carrier of (X)
x is Element of the carrier of (X)
ft is Element of the carrier of (X)
x is Element of the carrier of (X)
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
(X) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober first-countable Frechet sequential strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
Y is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
Lim Y is Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
lim Y is Element of the carrier of (X)
f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
Lim f is Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
lim f is Element of the carrier of (X)
ft is Element of the carrier of (X)
x is Element of the carrier of (X)
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
G is Element of the carrier of (X)
{G} is non empty Element of bool the carrier of (X)
{(lim f)} is non empty Element of bool the carrier of (X)
xt is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
lim xt is Element of the carrier of X
{(lim xt)} is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
(X) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober first-countable Frechet sequential strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
Y is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
ft is Element of the carrier of X
x is Element of the carrier of (X)
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
G is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
xt is Element of the carrier of (X)
Gt is V27() real ext-real Element of REAL
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
(X) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober first-countable Frechet sequential strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
Y is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
ft is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
(X) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober first-countable Frechet sequential strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
Y is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
lim Y is Element of the carrier of X
{(lim Y)} is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
Lim f is Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
lim f is Element of the carrier of (X)
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
[:NAT, the carrier of (X):] is non empty set
bool [:NAT, the carrier of (X):] is non empty set
ft is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]
Lim ft is Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
lim ft is Element of the carrier of (X)
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
(X) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober first-countable Frechet sequential strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is Element of bool the carrier of X
f is Element of bool the carrier of (X)
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
ft is Element of bool the carrier of (X)
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
(X) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober first-countable Frechet sequential strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is Element of bool the carrier of X
f is Element of bool the carrier of (X)
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
ft is Element of bool the carrier of (X)
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
(X) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober first-countable Frechet sequential strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
Y is Element of bool the carrier of (X)
f is Element of bool the carrier of (X)
ft is Element of the carrier of (X)
x is Element of the carrier of (X)
xt is Element of bool the carrier of (X)
G is open Element of bool the carrier of (X)
xt is Element of bool the carrier of (X)
G is open Element of bool the carrier of (X)
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
Y is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(Y) is non empty TopSpace-like sequential TopStruct
(Y) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of Y is non empty set
(Y) is V10() V13([: the carrier of Y, the carrier of Y:]) V14( REAL ) Function-like V46([: the carrier of Y, the carrier of Y:], REAL ) Element of bool [:[: the carrier of Y, the carrier of Y:],REAL:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:],REAL:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:],REAL:] is non empty set
MetrStruct(# the carrier of Y,(Y) #) is strict MetrStruct
TopSpaceMetr (Y) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (Y) is non empty set
Family_open_set (Y) is Element of bool (bool the carrier of (Y))
bool the carrier of (Y) is non empty set
bool (bool the carrier of (Y)) is non empty set
TopStruct(# the carrier of (Y),(Family_open_set (Y)) #) is strict TopStruct
the carrier of (Y) is non empty set
[: the carrier of (X), the carrier of (Y):] is non empty set
bool [: the carrier of (X), the carrier of (Y):] is non empty set
(X) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober first-countable Frechet sequential strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
(Y) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober first-countable Frechet sequential strict add-continuous Mult-continuous RLTopStruct
the carrier of (Y) is non empty set
[: the carrier of (X), the carrier of (Y):] is non empty set
bool [: the carrier of (X), the carrier of (Y):] is non empty set
f is V10() V13( the carrier of (X)) V14( the carrier of (Y)) Function-like V46( the carrier of (X), the carrier of (Y)) Element of bool [: the carrier of (X), the carrier of (Y):]
ft is V10() V13( the carrier of (X)) V14( the carrier of (Y)) Function-like V46( the carrier of (X), the carrier of (Y)) Element of bool [: the carrier of (X), the carrier of (Y):]
x is Element of the carrier of (X)
xt is Element of the carrier of (X)
ft . xt is Element of the carrier of (Y)
G is a_neighborhood of ft . xt
bool the carrier of (Y) is non empty set
f . x is Element of the carrier of (Y)
Gt is a_neighborhood of f . x
Ht is a_neighborhood of x
f .: Ht is Element of bool the carrier of (Y)
bool the carrier of (X) is non empty set
H is a_neighborhood of xt
H is a_neighborhood of xt
ft .: H is Element of bool the carrier of (Y)
bool the carrier of (Y) is non empty set
G is a_neighborhood of f . x
Gt is a_neighborhood of ft . xt
Ht is a_neighborhood of xt
ft .: Ht is Element of bool the carrier of (Y)
bool the carrier of (X) is non empty set
H is a_neighborhood of x
H is a_neighborhood of x
f .: H is Element of bool the carrier of (Y)
X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(X) is non empty TopSpace-like sequential TopStruct
(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of X is non empty set
(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is non empty set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(X) #) is strict MetrStruct
TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (X) is non empty set
Family_open_set (X) is Element of bool (bool the carrier of (X))
bool the carrier of (X) is non empty set
bool (bool the carrier of (X)) is non empty set
TopStruct(# the carrier of (X),(Family_open_set (X)) #) is strict TopStruct
the carrier of (X) is non empty set
Y is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR
(Y) is non empty TopSpace-like sequential TopStruct
(Y) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of Y is non empty set
(Y) is V10() V13([: the carrier of Y, the carrier of Y:]) V14( REAL ) Function-like V46([: the carrier of Y, the carrier of Y:], REAL ) Element of bool [:[: the carrier of Y, the carrier of Y:],REAL:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:],REAL:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:],REAL:] is non empty set
MetrStruct(# the carrier of Y,(Y) #) is strict MetrStruct
TopSpaceMetr (Y) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct
the carrier of (Y) is non empty set
Family_open_set (Y) is Element of bool (bool the carrier of (Y))
bool the carrier of (Y) is non empty set
bool (bool the carrier of (Y)) is non empty set
TopStruct(# the carrier of (Y),(Family_open_set (Y)) #) is strict TopStruct
the carrier of (Y) is non empty set
[: the carrier of (X), the carrier of (Y):] is non empty set
bool [: the carrier of (X), the carrier of (Y):] is non empty set
(X) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober first-countable Frechet sequential strict add-continuous Mult-continuous RLTopStruct
the carrier of (X) is non empty set
(Y) is non empty TopSpace-like T_2 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital sober first-countable Frechet sequential strict add-continuous Mult-continuous RLTopStruct
the carrier of (Y) is non empty set
[: the carrier of (X), the carrier of (Y):] is non empty set
bool [: the carrier of (X), the carrier of (Y):] is non empty set
f is V10() V13( the carrier of (X)) V14( the carrier of (Y)) Function-like V46( the carrier of (X), the carrier of (Y)) Element of bool [: the carrier of (X), the carrier of (Y):]
ft is V10() V13( the carrier of (X)) V14( the carrier of (Y)) Function-like V46( the carrier of (X), the carrier of (Y)) Element of bool [: the carrier of (X), the carrier of (Y):]
x is Element of the carrier of (X)
xt is Element of the carrier of (X)
x is Element of the carrier of (X)
xt is Element of the carrier of (X)