:: LOPBAN_6 semantic presentation

REAL is set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL

bool REAL is non empty set

omega is non empty epsilon-transitive epsilon-connected ordinal set

bool omega is non empty set

1 is non empty epsilon-transitive epsilon-connected ordinal natural complex 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 set

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

[:REAL,REAL:] is set

[:[:REAL,REAL:],REAL:] is set

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

2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT

[:2,2:] is non empty set

[:[:2,2:],REAL:] is set

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

bool NAT is non empty set

[:NAT,REAL:] is set

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

COMPLEX is set

RAT is set

INT is set

K483() is non empty set

[:K483(),K483():] is non empty set

[:[:K483(),K483():],K483():] is non empty set

bool [:[:K483(),K483():],K483():] is non empty set

[:REAL,K483():] is set

[:[:REAL,K483():],K483():] is set

bool [:[:REAL,K483():],K483():] is non empty set

K489() is L14()

the carrier of K489() is set

bool the carrier of K489() is non empty set

K493() is Element of bool the carrier of K489()

[:K493(),K493():] is set

[:[:K493(),K493():],REAL:] is set

bool [:[:K493(),K493():],REAL:] is non empty set

the_set_of_l1RealSequences is Element of bool the carrier of K489()

[:the_set_of_l1RealSequences,REAL:] is set

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

{} is set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative set

0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT

- 1 is complex real ext-real non positive Element of REAL

X is complex real ext-real set

Y is complex real ext-real set

T is complex real ext-real set

1 + T is complex real ext-real Element of REAL

Y * (1 + T) is complex real ext-real Element of REAL

Y / (1 + T) is complex real ext-real Element of REAL

T / X is complex real ext-real Element of COMPLEX

(T / X) - 1 is complex real ext-real Element of REAL

1 + ((T / X) - 1) is complex real ext-real Element of REAL

(1 + ((T / X) - 1)) " is complex real ext-real Element of REAL

1 / (1 + ((T / X) - 1)) is complex real ext-real Element of REAL

T * ((1 + ((T / X) - 1)) ") is complex real ext-real Element of REAL

T * 1 is complex real ext-real Element of REAL

(T * 1) / (1 + ((T / X) - 1)) is complex real ext-real Element of REAL

(1 + ((T / X) - 1)) * X is complex real ext-real Element of REAL

X / X is complex real ext-real Element of COMPLEX

(X / X) * T is complex real ext-real set

1 * T is complex real ext-real Element of REAL

((1 + ((T / X) - 1)) ") * (1 + ((T / X) - 1)) is complex real ext-real Element of REAL

(((1 + ((T / X) - 1)) ") * (1 + ((T / X) - 1))) * X is complex real ext-real Element of REAL

Y * (1 + ((T / X) - 1)) is complex real ext-real Element of REAL

Y / (1 + ((T / X) - 1)) is complex real ext-real Element of REAL

1 + T is complex real ext-real Element of REAL

Y / (1 + T) is complex real ext-real Element of REAL

T / X is complex real ext-real Element of COMPLEX

(T / X) - 1 is complex real ext-real Element of REAL

1 + ((T / X) - 1) is complex real ext-real Element of REAL

Y / (1 + ((T / X) - 1)) is complex real ext-real Element of REAL

1 + T is complex real ext-real Element of REAL

Y / (1 + T) is complex real ext-real Element of REAL

T / X is complex real ext-real Element of COMPLEX

(T / X) - 1 is complex real ext-real Element of REAL

1 + ((T / X) - 1) is complex real ext-real Element of REAL

Y / (1 + ((T / X) - 1)) is complex real ext-real Element of REAL

T is complex real ext-real set

1 + T is complex real ext-real Element of REAL

Y / (1 + T) is complex real ext-real Element of REAL

F

[:NAT,F

bool [:NAT,F

F

F

[:F

X is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT

Y is Element of [:F

Y `1 is set

Y `2 is set

Y `1 is Element of F

Y `2 is Element of F

TB1 is Element of F

G is Element of F

f is Element of F

[G,f] is V13() Element of [:F

{G,f} is set

{G} is set

{{G,f},{G}} is set

n0 is Element of [:F

n0 `2 is set

n0 `1 is set

[:NAT,[:F

bool [:NAT,[:F

[F

{F

{F

{{F

X is non empty V16() V19( NAT ) V20([:F

X . 0 is Element of [:F

Y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT

X . Y is Element of [:F

(X . Y) `1 is Element of F

Y is non empty V16() V19( NAT ) V20(F

T is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT

Y . T is Element of F

X . T is Element of [:F

(X . T) `1 is Element of F

T + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT

X . (T + 1) is Element of [:F

(T + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT

X . ((T + 1) + 1) is Element of [:F

(X . (T + 1)) `1 is set

(X . (T + 1)) `2 is set

(X . ((T + 1) + 1)) `2 is set

(X . ((T + 1) + 1)) `1 is set

T + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT

Y . (T + 2) is Element of F

(X . (T + 1)) `2 is Element of F

Y . (T + 1) is Element of F

(X . (T + 1)) `1 is Element of F

(X . T) `2 is Element of F

Y . 0 is Element of F

Y . 1 is Element of F

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT

X . (0 + 1) is Element of [:F

(X . 0) `1 is set

(X . 0) `2 is set

(X . (0 + 1)) `2 is set

(X . (0 + 1)) `1 is set

(X . 0) `1 is Element of F

X . 1 is Element of [:F

(X . 1) `1 is Element of F

T is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT

Y . T is Element of F

T + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT

Y . (T + 1) is Element of F

T + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT

Y . (T + 2) is Element of F

X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR

the carrier of X is non empty set

0. X is zero Element of the carrier of X

Y is Element of the carrier of X

T is complex real ext-real set

Ball (Y,T) is Element of bool the carrier of X

bool the carrier of X is non empty set

{ b

Ball ((0. X),T) is Element of bool the carrier of X

{ b

Y + (Ball ((0. X),T)) is Element of bool the carrier of X

{ K230(X,Y,b

T1 is set

TB1 is Element of the carrier of X

TB1 - Y is Element of the carrier of X

- Y is Element of the carrier of X

K230(X,TB1,(- Y)) is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,TB1,(- Y)) is Element of the carrier of X

- (TB1 - Y) is Element of the carrier of X

||.(- (TB1 - Y)).|| is complex real ext-real non negative 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

K230(X,Y,(- f)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,Y,(- f)) is Element of the carrier of X

||.(Y - f).|| is complex real ext-real non negative Element of REAL

(0. X) - (TB1 - Y) is Element of the carrier of X

K230(X,(0. X),(- (TB1 - Y))) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(0. X),(- (TB1 - Y))) is Element of the carrier of X

||.((0. X) - (TB1 - Y)).|| is complex real ext-real non negative Element of REAL

(TB1 - Y) + Y is Element of the carrier of X

K179( the carrier of X, the U7 of X,(TB1 - Y),Y) is Element of the carrier of X

(- Y) + Y is Element of the carrier of X

K179( the carrier of X, the U7 of X,(- Y),Y) is Element of the carrier of X

TB1 + ((- Y) + Y) is Element of the carrier of X

K179( the carrier of X, the U7 of X,TB1,((- Y) + Y)) is Element of the carrier of X

TB1 + (0. X) is Element of the carrier of X

K179( the carrier of X, the U7 of X,TB1,(0. X)) is Element of the carrier of X

T1 is set

TB1 is Element of the carrier of X

Y + TB1 is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,Y,TB1) is Element of the carrier of X

TB1 + Y is Element of the carrier of X

K179( the carrier of X, the U7 of X,TB1,Y) is Element of the carrier of X

- TB1 is Element of the carrier of X

||.(- TB1).|| is complex real ext-real non negative Element of REAL

f is Element of the carrier of X

(0. X) - f is Element of the carrier of X

- f is Element of the carrier of X

K230(X,(0. X),(- f)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(0. X),(- f)) is Element of the carrier of X

||.((0. X) - f).|| is complex real ext-real non negative Element of REAL

||.TB1.|| is complex real ext-real non negative Element of REAL

TB1 + (0. X) is Element of the carrier of X

K179( the carrier of X, the U7 of X,TB1,(0. X)) is Element of the carrier of X

||.(TB1 + (0. X)).|| is complex real ext-real non negative Element of REAL

- Y is Element of the carrier of X

Y + (- Y) is Element of the carrier of X

K179( the carrier of X, the U7 of X,Y,(- Y)) is Element of the carrier of X

TB1 + (Y + (- Y)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,TB1,(Y + (- Y))) is Element of the carrier of X

||.(TB1 + (Y + (- Y))).|| is complex real ext-real non negative Element of REAL

(TB1 + Y) - Y is Element of the carrier of X

K230(X,(TB1 + Y),(- Y)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(TB1 + Y),(- Y)) is Element of the carrier of X

||.((TB1 + Y) - Y).|| is complex real ext-real non negative Element of REAL

Y - (TB1 + Y) is Element of the carrier of X

- (TB1 + Y) is Element of the carrier of X

K230(X,Y,(- (TB1 + Y))) is Element of the carrier of X

K179( the carrier of X, the U7 of X,Y,(- (TB1 + Y))) is Element of the carrier of X

||.(Y - (TB1 + Y)).|| is complex real ext-real non negative Element of REAL

X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR

0. X is zero Element of the carrier of X

the carrier of X is non empty set

Y is complex real ext-real set

Ball ((0. X),Y) is Element of bool the carrier of X

bool the carrier of X is non empty set

{ b

T is complex real ext-real Element of REAL

T * Y is complex real ext-real Element of REAL

Ball ((0. X),(T * Y)) is Element of bool the carrier of X

{ b

T * (Ball ((0. X),Y)) is Element of bool the carrier of X

{ (T * b

T1 is set

TB1 is Element of the carrier of X

- TB1 is Element of the carrier of X

||.(- TB1).|| is complex real ext-real non negative Element of REAL

G is Element of the carrier of X

(0. X) - G is Element of the carrier of X

- G is Element of the carrier of X

K230(X,(0. X),(- G)) is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,(0. X),(- G)) is Element of the carrier of X

||.((0. X) - G).|| is complex real ext-real non negative Element of REAL

||.TB1.|| is complex real ext-real non negative Element of REAL

T " is complex real ext-real Element of REAL

(T ") * (T * Y) is complex real ext-real Element of REAL

(T ") * ||.TB1.|| is complex real ext-real Element of REAL

T * (T ") is complex real ext-real Element of REAL

(T * (T ")) * Y is complex real ext-real Element of REAL

1 * Y is complex real ext-real Element of REAL

(T ") * TB1 is Element of the carrier of X

the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:REAL, the carrier of X:] is set

[:[:REAL, the carrier of X:], the carrier of X:] is set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

K175( the U9 of X,(T "),TB1) is set

||.((T ") * TB1).|| is complex real ext-real non negative Element of REAL

abs (T ") is complex real ext-real Element of REAL

(abs (T ")) * ||.TB1.|| is complex real ext-real Element of REAL

- ((T ") * TB1) is Element of the carrier of X

||.(- ((T ") * TB1)).|| is complex real ext-real non negative Element of REAL

(0. X) - ((T ") * TB1) is Element of the carrier of X

K230(X,(0. X),(- ((T ") * TB1))) is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,(0. X),(- ((T ") * TB1))) is Element of the carrier of X

||.((0. X) - ((T ") * TB1)).|| is complex real ext-real non negative Element of REAL

T * ((T ") * TB1) is Element of the carrier of X

K175( the U9 of X,T,((T ") * TB1)) is set

(T * (T ")) * TB1 is Element of the carrier of X

K175( the U9 of X,(T * (T ")),TB1) is set

1 * TB1 is Element of the carrier of X

K175( the U9 of X,1,TB1) is set

T1 is set

TB1 is Element of the carrier of X

G is Element of the carrier of X

T * G is Element of the carrier of X

the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:REAL, the carrier of X:] is set

[:[:REAL, the carrier of X:], the carrier of X:] is set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

K175( the U9 of X,T,G) is set

- G is Element of the carrier of X

||.(- G).|| is complex real ext-real non negative Element of REAL

f is Element of the carrier of X

(0. X) - f is Element of the carrier of X

- f is Element of the carrier of X

K230(X,(0. X),(- f)) is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,(0. X),(- f)) is Element of the carrier of X

||.((0. X) - f).|| is complex real ext-real non negative Element of REAL

||.G.|| is complex real ext-real non negative Element of REAL

||.TB1.|| is complex real ext-real non negative Element of REAL

abs T is complex real ext-real Element of REAL

(abs T) * ||.G.|| is complex real ext-real Element of REAL

T * ||.G.|| is complex real ext-real Element of REAL

- TB1 is Element of the carrier of X

||.(- TB1).|| is complex real ext-real non negative Element of REAL

(0. X) - TB1 is Element of the carrier of X

K230(X,(0. X),(- TB1)) is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,(0. X),(- TB1)) is Element of the carrier of X

||.((0. X) - TB1).|| is complex real ext-real non negative Element of REAL

X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR

the carrier of X is non empty set

bool the carrier of X is non empty set

Y is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() 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

T is non empty V16() V19( the carrier of X) V20( the carrier of Y) Function-like V26( the carrier of X) quasi_total V231(X,Y) V232(X,Y) Element of bool [: the carrier of X, the carrier of Y:]

T1 is Element of bool the carrier of X

TB1 is Element of bool the carrier of X

T1 + TB1 is Element of bool the carrier of X

{ K230(X,b

T .: (T1 + TB1) is Element of bool the carrier of Y

bool the carrier of Y is non empty set

T .: T1 is Element of bool the carrier of Y

T .: TB1 is Element of bool the carrier of Y

(T .: T1) + (T .: TB1) is Element of bool the carrier of Y

{ K230(Y,b

G is set

f is set

T . f is set

f is Element of the carrier of X

n0 is Element of the carrier of X

f + n0 is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,f,n0) is Element of the carrier of X

T . f is Element of the carrier of Y

T . n0 is Element of the carrier of Y

(T . f) + (T . n0) is Element of the carrier of Y

the U7 of Y is non empty V16() V19([: the carrier of Y, the carrier of Y:]) V20( the carrier of Y) Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]

[: the carrier of Y, the carrier of Y:] is non empty set

[:[: 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

K179( the carrier of Y, the U7 of Y,(T . f),(T . n0)) is Element of the carrier of Y

G is set

f is Element of the carrier of Y

f is Element of the carrier of Y

f + f is Element of the carrier of Y

the U7 of Y is non empty V16() V19([: the carrier of Y, the carrier of Y:]) V20( the carrier of Y) Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]

[: the carrier of Y, the carrier of Y:] is non empty set

[:[: 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

K179( the carrier of Y, the U7 of Y,f,f) is Element of the carrier of Y

n0 is Element of the carrier of X

T . n0 is Element of the carrier of Y

r is Element of the carrier of X

T . r is Element of the carrier of Y

TBn0 is Element of the carrier of X

y0 is Element of the carrier of X

TBn0 + y0 is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,TBn0,y0) is Element of the carrier of X

T . (TBn0 + y0) is Element of the carrier of Y

X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR

the carrier of X is non empty set

bool the carrier of X is non empty set

Y is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() 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

T is non empty V16() V19( the carrier of X) V20( the carrier of Y) Function-like V26( the carrier of X) quasi_total V231(X,Y) V232(X,Y) Element of bool [: the carrier of X, the carrier of Y:]

T1 is Element of bool the carrier of X

T .: T1 is Element of bool the carrier of Y

bool the carrier of Y is non empty set

TB1 is complex real ext-real Element of REAL

TB1 * T1 is Element of bool the carrier of X

{ (TB1 * b

T .: (TB1 * T1) is Element of bool the carrier of Y

TB1 * (T .: T1) is Element of bool the carrier of Y

{ (TB1 * b

G is set

f is set

T . f is set

f is Element of the carrier of X

TB1 * f is Element of the carrier of X

the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:REAL, the carrier of X:] is set

[:[:REAL, the carrier of X:], the carrier of X:] is set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

K175( the U9 of X,TB1,f) is set

T . f is Element of the carrier of Y

TB1 * (T . f) is Element of the carrier of Y

the U9 of Y is V16() V19([:REAL, the carrier of Y:]) V20( the carrier of Y) Function-like V26([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]

[:REAL, the carrier of Y:] is set

[:[:REAL, the carrier of Y:], the carrier of Y:] is set

bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set

K175( the U9 of Y,TB1,(T . f)) is set

G is set

f is Element of the carrier of Y

TB1 * f is Element of the carrier of Y

the U9 of Y is V16() V19([:REAL, the carrier of Y:]) V20( the carrier of Y) Function-like V26([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]

[:REAL, the carrier of Y:] is set

[:[:REAL, the carrier of Y:], the carrier of Y:] is set

bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set

K175( the U9 of Y,TB1,f) is set

f is Element of the carrier of X

T . f is Element of the carrier of Y

n0 is Element of the carrier of X

TB1 * n0 is Element of the carrier of X

the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:REAL, the carrier of X:] is set

[:[:REAL, the carrier of X:], the carrier of X:] is set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

K175( the U9 of X,TB1,n0) is set

T . (TB1 * n0) is Element of the carrier of Y

X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR

the carrier of X is non empty set

bool the carrier of X is non empty set

Y is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() 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

T is non empty V16() V19( the carrier of X) V20( the carrier of Y) Function-like V26( the carrier of X) quasi_total V231(X,Y) V232(X,Y) Element of bool [: the carrier of X, the carrier of Y:]

T1 is Element of bool the carrier of X

T .: T1 is Element of bool the carrier of Y

bool the carrier of Y is non empty set

TB1 is Element of the carrier of X

TB1 + T1 is Element of bool the carrier of X

{ K230(X,TB1,b

T .: (TB1 + T1) is Element of bool the carrier of Y

T . TB1 is Element of the carrier of Y

(T . TB1) + (T .: T1) is Element of bool the carrier of Y

{ K230(Y,(T . TB1),b

G is set

f is set

T . f is set

f is Element of the carrier of X

n0 is Element of the carrier of X

TB1 + n0 is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,TB1,n0) is Element of the carrier of X

T . n0 is Element of the carrier of Y

(T . TB1) + (T . n0) is Element of the carrier of Y

the U7 of Y is non empty V16() V19([: the carrier of Y, the carrier of Y:]) V20( the carrier of Y) Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]

[: the carrier of Y, the carrier of Y:] is non empty set

[:[: 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

K179( the carrier of Y, the U7 of Y,(T . TB1),(T . n0)) is Element of the carrier of Y

G is set

f is Element of the carrier of Y

(T . TB1) + f is Element of the carrier of Y

the U7 of Y is non empty V16() V19([: the carrier of Y, the carrier of Y:]) V20( the carrier of Y) Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]

[: the carrier of Y, the carrier of Y:] is non empty set

[:[: 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

K179( the carrier of Y, the U7 of Y,(T . TB1),f) is Element of the carrier of Y

f is Element of the carrier of X

T . f is Element of the carrier of Y

TB1 + f is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,TB1,f) is Element of the carrier of X

T . (TB1 + f) is Element of the carrier of Y

X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR

the carrier of X is non empty set

bool the carrier of X is non empty set

LinearTopSpaceNorm X is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()

the carrier of (LinearTopSpaceNorm X) is non empty set

bool the carrier of (LinearTopSpaceNorm X) is non empty set

Y is Element of bool the carrier of X

T is Element of bool the carrier of X

Y + T is Element of bool the carrier of X

{ K230(X,b

T1 is Element of bool the carrier of (LinearTopSpaceNorm X)

TB1 is Element of bool the carrier of (LinearTopSpaceNorm X)

T1 + TB1 is Element of bool the carrier of (LinearTopSpaceNorm X)

{ K230((LinearTopSpaceNorm X),b

G is set

f is Element of the carrier of X

f is Element of the carrier of X

f + f is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,f,f) is Element of the carrier of X

r is Element of the carrier of (LinearTopSpaceNorm X)

n0 is Element of the carrier of (LinearTopSpaceNorm X)

r + n0 is Element of the carrier of (LinearTopSpaceNorm X)

the U7 of (LinearTopSpaceNorm X) is non empty V16() V19([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]

[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):] is non empty set

[:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set

bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set

K179( the carrier of (LinearTopSpaceNorm X), the U7 of (LinearTopSpaceNorm X),r,n0) is Element of the carrier of (LinearTopSpaceNorm X)

G is set

f is Element of the carrier of (LinearTopSpaceNorm X)

f is Element of the carrier of (LinearTopSpaceNorm X)

f + f is Element of the carrier of (LinearTopSpaceNorm X)

the U7 of (LinearTopSpaceNorm X) is non empty V16() V19([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]

[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):] is non empty set

[:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set

bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set

K179( the carrier of (LinearTopSpaceNorm X), the U7 of (LinearTopSpaceNorm X),f,f) is Element of the carrier of (LinearTopSpaceNorm X)

r is Element of the carrier of X

n0 is Element of the carrier of X

r + n0 is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,r,n0) is Element of the carrier of X

X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR

the carrier of X is non empty set

bool the carrier of X is non empty set

LinearTopSpaceNorm X is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()

the carrier of (LinearTopSpaceNorm X) is non empty set

bool the carrier of (LinearTopSpaceNorm X) is non empty set

Y is Element of bool the carrier of X

T is Element of the carrier of X

T + Y is Element of bool the carrier of X

{ K230(X,T,b

T1 is Element of bool the carrier of (LinearTopSpaceNorm X)

TB1 is Element of the carrier of (LinearTopSpaceNorm X)

TB1 + T1 is Element of bool the carrier of (LinearTopSpaceNorm X)

{ K230((LinearTopSpaceNorm X),TB1,b

G is set

f is Element of the carrier of X

T + f is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,T,f) is Element of the carrier of X

f is Element of the carrier of (LinearTopSpaceNorm X)

TB1 + f is Element of the carrier of (LinearTopSpaceNorm X)

the U7 of (LinearTopSpaceNorm X) is non empty V16() V19([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]

[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):] is non empty set

[:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set

bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set

K179( the carrier of (LinearTopSpaceNorm X), the U7 of (LinearTopSpaceNorm X),TB1,f) is Element of the carrier of (LinearTopSpaceNorm X)

G is set

f is Element of the carrier of (LinearTopSpaceNorm X)

TB1 + f is Element of the carrier of (LinearTopSpaceNorm X)

the U7 of (LinearTopSpaceNorm X) is non empty V16() V19([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]

[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):] is non empty set

[:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set

bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set

K179( the carrier of (LinearTopSpaceNorm X), the U7 of (LinearTopSpaceNorm X),TB1,f) is Element of the carrier of (LinearTopSpaceNorm X)

f is Element of the carrier of X

T + f is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,T,f) is Element of the carrier of X

X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR

the carrier of X is non empty set

bool the carrier of X is non empty set

LinearTopSpaceNorm X is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()

the carrier of (LinearTopSpaceNorm X) is non empty set

bool the carrier of (LinearTopSpaceNorm X) is non empty set

Y is Element of bool the carrier of X

T is complex real ext-real Element of REAL

T * Y is Element of bool the carrier of X

{ (T * b

T1 is Element of bool the carrier of (LinearTopSpaceNorm X)

T * T1 is Element of bool the carrier of (LinearTopSpaceNorm X)

{ (T * b

TB1 is set

G is Element of the carrier of X

T * G is Element of the carrier of X

the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:REAL, the carrier of X:] is set

[:[:REAL, the carrier of X:], the carrier of X:] is set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

K175( the U9 of X,T,G) is set

f is Element of the carrier of (LinearTopSpaceNorm X)

T * f is Element of the carrier of (LinearTopSpaceNorm X)

the U9 of (LinearTopSpaceNorm X) is V16() V19([:REAL, the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([:REAL, the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]

[:REAL, the carrier of (LinearTopSpaceNorm X):] is set

[:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is set

bool [:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set

K175( the U9 of (LinearTopSpaceNorm X),T,f) is set

TB1 is set

G is Element of the carrier of (LinearTopSpaceNorm X)

T * G is Element of the carrier of (LinearTopSpaceNorm X)

the U9 of (LinearTopSpaceNorm X) is V16() V19([:REAL, the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([:REAL, the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]

[:REAL, the carrier of (LinearTopSpaceNorm X):] is set

[:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is set

bool [:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set

K175( the U9 of (LinearTopSpaceNorm X),T,G) is set

f is Element of the carrier of X

T * f is Element of the carrier of X

the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:REAL, the carrier of X:] is set

[:[:REAL, the carrier of X:], the carrier of X:] is set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

K175( the U9 of X,T,f) is set

X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR

TopSpaceNorm X is non empty TopSpace-like TopStruct

MetricSpaceNorm X is non empty V88() V89() V90() V91() L7()

the carrier of X is non empty set

distance_by_norm_of X is V16() V19([: the carrier of X, the carrier of X:]) V20( REAL ) Function-like quasi_total 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 set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

G7( the carrier of X,(distance_by_norm_of X)) is V83() L7()

K210((MetricSpaceNorm X)) is TopStruct

the carrier of (MetricSpaceNorm X) is non empty set

K209((MetricSpaceNorm X)) is Element of bool (bool the carrier of (MetricSpaceNorm X))

bool the carrier of (MetricSpaceNorm X) is non empty set

bool (bool the carrier of (MetricSpaceNorm X)) is non empty set

TopStruct(# the carrier of (MetricSpaceNorm X),K209((MetricSpaceNorm X)) #) is strict TopStruct

the carrier of (TopSpaceNorm X) is non empty set

bool the carrier of (TopSpaceNorm X) is non empty set

LinearTopSpaceNorm X is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()

the carrier of (LinearTopSpaceNorm X) is non empty set

bool the carrier of (LinearTopSpaceNorm X) is non empty set

Y is Element of bool the carrier of (TopSpaceNorm X)

Cl Y is closed Element of bool the carrier of (TopSpaceNorm X)

T is Element of bool the carrier of (LinearTopSpaceNorm X)

Cl T is closed Element of bool the carrier of (LinearTopSpaceNorm X)

T1 is set

TB1 is Element of bool the carrier of (LinearTopSpaceNorm X)

bool the carrier of X is non empty set

G is Element of bool the carrier of X

f is Element of bool the carrier of (TopSpaceNorm X)

T1 is set

TB1 is Element of bool the carrier of (TopSpaceNorm X)

bool the carrier of X is non empty set

G is Element of bool the carrier of X

f is Element of bool the carrier of (LinearTopSpaceNorm X)

X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR

the carrier of X is non empty set

0. X is zero Element of the carrier of X

T is complex real ext-real set

Ball ((0. X),T) is Element of bool the carrier of X

bool the carrier of X is non empty set

{ b

(- 1) * (Ball ((0. X),T)) is Element of bool the carrier of X

{ ((- 1) * b

T1 is set

TB1 is Element of the carrier of X

- TB1 is Element of the carrier of X

||.(- TB1).|| is complex real ext-real non negative Element of REAL

G is Element of the carrier of X

(0. X) - G is Element of the carrier of X

- G is Element of the carrier of X

K230(X,(0. X),(- G)) is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,(0. X),(- G)) is Element of the carrier of X

||.((0. X) - G).|| is complex real ext-real non negative Element of REAL

- (- TB1) is Element of the carrier of X

||.(- (- TB1)).|| is complex real ext-real non negative Element of REAL

(0. X) - (- TB1) is Element of the carrier of X

K230(X,(0. X),(- (- TB1))) is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,(0. X),(- (- TB1))) is Element of the carrier of X

||.((0. X) - (- TB1)).|| is complex real ext-real non negative Element of REAL

(- 1) * (- TB1) is Element of the carrier of X

the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:REAL, the carrier of X:] is set

[:[:REAL, the carrier of X:], the carrier of X:] is set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

K175( the U9 of X,(- 1),(- TB1)) is set

1 * TB1 is Element of the carrier of X

K175( the U9 of X,1,TB1) is set

T1 is set

TB1 is Element of the carrier of X

G is Element of the carrier of X

(- 1) * G is Element of the carrier of X

the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:REAL, the carrier of X:] is set

[:[:REAL, the carrier of X:], the carrier of X:] is set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

K175( the U9 of X,(- 1),G) is set

- G is Element of the carrier of X

||.(- G).|| is complex real ext-real non negative Element of REAL

f is Element of the carrier of X

(0. X) - f is Element of the carrier of X

- f is Element of the carrier of X

K230(X,(0. X),(- f)) is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,(0. X),(- f)) is Element of the carrier of X

||.((0. X) - f).|| is complex real ext-real non negative Element of REAL

- (- G) is Element of the carrier of X

||.(- (- G)).|| is complex real ext-real non negative Element of REAL

(0. X) - (- G) is Element of the carrier of X

K230(X,(0. X),(- (- G))) is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,(0. X),(- (- G))) is Element of the carrier of X

||.((0. X) - (- G)).|| is complex real ext-real non negative Element of REAL

X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR

the carrier of X is non empty set

LinearTopSpaceNorm X is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()

the carrier of (LinearTopSpaceNorm X) is non empty set

bool the carrier of (LinearTopSpaceNorm X) is non empty set

Y is Element of the carrier of X

T is complex real ext-real set

Ball (Y,T) is Element of bool the carrier of X

bool the carrier of X is non empty set

{ b

T1 is Element of bool the carrier of (LinearTopSpaceNorm X)

TB1 is Element of bool the carrier of X

G is Element of the carrier of X

f is Element of the carrier of X

f is complex real ext-real Element of REAL

f * G is Element of the carrier of X

the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:REAL, the carrier of X:] is set

[:[:REAL, the carrier of X:], the carrier of X:] is set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

K175( the U9 of X,f,G) is set

1 - f is complex real ext-real Element of REAL

(1 - f) * f is Element of the carrier of X

K175( the U9 of X,(1 - f),f) is set

(f * G) + ((1 - f) * f) is Element of the carrier of X

the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total 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

K179( the carrier of X, the U7 of X,(f * G),((1 - f) * f)) is Element of the carrier of X

abs f is complex real ext-real Element of REAL

(abs f) * T is complex real ext-real Element of REAL

Y - G is Element of the carrier of X

- G is Element of the carrier of X

K230(X,Y,(- G)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,Y,(- G)) is Element of the carrier of X

||.(Y - G).|| is complex real ext-real non negative Element of REAL

(abs f) * ||.(Y - G).|| is complex real ext-real Element of REAL

n0 is Element of the carrier of X

Y - n0 is Element of the carrier of X

- n0 is Element of the carrier of X

K230(X,Y,(- n0)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,Y,(- n0)) is Element of the carrier of X

||.(Y - n0).|| is complex real ext-real non negative Element of REAL

f + 0 is complex real ext-real Element of REAL

abs (1 - f) is complex real ext-real Element of REAL

(abs (1 - f)) * T is complex real ext-real Element of REAL

Y - f is Element of the carrier of X

- f is Element of the carrier of X

K230(X,Y,(- f)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,Y,(- f)) is Element of the carrier of X

||.(Y - f).|| is complex real ext-real non negative Element of REAL

(abs (1 - f)) * ||.(Y - f).|| is complex real ext-real Element of REAL

n0 is Element of the carrier of X

Y - n0 is Element of the carrier of X

- n0 is Element of the carrier of X

K230(X,Y,(- n0)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,Y,(- n0)) is Element of the carrier of X

||.(Y - n0).|| is complex real ext-real non negative Element of REAL

((abs f) * T) + ((abs (1 - f)) * T) is complex real ext-real Element of REAL

((abs f) * ||.(Y - G).||) + ((abs (1 - f)) * ||.(Y - f).||) is complex real ext-real Element of REAL

f * T is complex real ext-real Element of REAL

(f * T) + ((abs (1 - f)) * T) is complex real ext-real Element of REAL

(1 - f) * T is complex real ext-real Element of REAL

(f * T) + ((1 - f) * T) is complex real ext-real Element of REAL

1 * T is complex real ext-real Element of REAL

f * (Y - G) is Element of the carrier of X

K175( the U9 of X,f,(Y - G)) is set

||.(f * (Y - G)).|| is complex real ext-real non negative Element of REAL

||.(f * (Y - G)).|| + ((abs (1 - f)) * ||.(Y - f).||) is complex real ext-real Element of REAL

(1 - f) * (Y - f) is Element of the carrier of X

K175( the U9 of X,(1 - f),(Y - f)) is set

||.((1 - f) * (Y - f)).|| is complex real ext-real non negative Element of REAL

||.(f * (Y - G)).|| + ||.((1 - f) * (Y - f)).|| is complex real ext-real non negative Element of REAL

f * Y is Element of the carrier of X

K175( the U9 of X,f,Y) is set

(1 - f) * Y is Element of the carrier of X

K175( the U9 of X,(1 - f),Y) is set

(f * Y) + ((1 - f) * Y) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(f * Y),((1 - f) * Y)) is Element of the carrier of X

((f * Y) + ((1 - f) * Y)) - ((f * G) + ((1 - f) * f)) is Element of the carrier of X

- ((f * G) + ((1 - f) * f)) is Element of the carrier of X

K230(X,((f * Y) + ((1 - f) * Y)),(- ((f * G) + ((1 - f) * f)))) is Element of the carrier of X

K179( the carrier of X, the U7 of X,((f * Y) + ((1 - f) * Y)),(- ((f * G) + ((1 - f) * f)))) is Element of the carrier of X

||.(((f * Y) + ((1 - f) * Y)) - ((f * G) + ((1 - f) * f))).|| is complex real ext-real non negative Element of REAL

(f * Y) + (- ((f * G) + ((1 - f) * f))) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(f * Y),(- ((f * G) + ((1 - f) * f)))) is Element of the carrier of X

((f * Y) + (- ((f * G) + ((1 - f) * f)))) + ((1 - f) * Y) is Element of the carrier of X

K179( the carrier of X, the U7 of X,((f * Y) + (- ((f * G) + ((1 - f) * f)))),((1 - f) * Y)) is Element of the carrier of X

||.(((f * Y) + (- ((f * G) + ((1 - f) * f)))) + ((1 - f) * Y)).|| is complex real ext-real non negative Element of REAL

(- 1) * ((f * G) + ((1 - f) * f)) is Element of the carrier of X

K175( the U9 of X,(- 1),((f * G) + ((1 - f) * f))) is set

(f * Y) + ((- 1) * ((f * G) + ((1 - f) * f))) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(f * Y),((- 1) * ((f * G) + ((1 - f) * f)))) is Element of the carrier of X

((f * Y) + ((- 1) * ((f * G) + ((1 - f) * f)))) + ((1 - f) * Y) is Element of the carrier of X

K179( the carrier of X, the U7 of X,((f * Y) + ((- 1) * ((f * G) + ((1 - f) * f)))),((1 - f) * Y)) is Element of the carrier of X

||.(((f * Y) + ((- 1) * ((f * G) + ((1 - f) * f)))) + ((1 - f) * Y)).|| is complex real ext-real non negative Element of REAL

(- 1) * (f * G) is Element of the carrier of X

K175( the U9 of X,(- 1),(f * G)) is set

(- 1) * ((1 - f) * f) is Element of the carrier of X

K175( the U9 of X,(- 1),((1 - f) * f)) is set

((- 1) * (f * G)) + ((- 1) * ((1 - f) * f)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,((- 1) * (f * G)),((- 1) * ((1 - f) * f))) is Element of the carrier of X

(f * Y) + (((- 1) * (f * G)) + ((- 1) * ((1 - f) * f))) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(f * Y),(((- 1) * (f * G)) + ((- 1) * ((1 - f) * f)))) is Element of the carrier of X

((f * Y) + (((- 1) * (f * G)) + ((- 1) * ((1 - f) * f)))) + ((1 - f) * Y) is Element of the carrier of X

K179( the carrier of X, the U7 of X,((f * Y) + (((- 1) * (f * G)) + ((- 1) * ((1 - f) * f)))),((1 - f) * Y)) is Element of the carrier of X

||.(((f * Y) + (((- 1) * (f * G)) + ((- 1) * ((1 - f) * f)))) + ((1 - f) * Y)).|| is complex real ext-real non negative Element of REAL

- (f * G) is Element of the carrier of X

(- (f * G)) + ((- 1) * ((1 - f) * f)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(- (f * G)),((- 1) * ((1 - f) * f))) is Element of the carrier of X

(f * Y) + ((- (f * G)) + ((- 1) * ((1 - f) * f))) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(f * Y),((- (f * G)) + ((- 1) * ((1 - f) * f)))) is Element of the carrier of X

((f * Y) + ((- (f * G)) + ((- 1) * ((1 - f) * f)))) + ((1 - f) * Y) is Element of the carrier of X

K179( the carrier of X, the U7 of X,((f * Y) + ((- (f * G)) + ((- 1) * ((1 - f) * f)))),((1 - f) * Y)) is Element of the carrier of X

||.(((f * Y) + ((- (f * G)) + ((- 1) * ((1 - f) * f)))) + ((1 - f) * Y)).|| is complex real ext-real non negative Element of REAL

- ((1 - f) * f) is Element of the carrier of X

(- (f * G)) + (- ((1 - f) * f)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(- (f * G)),(- ((1 - f) * f))) is Element of the carrier of X

(f * Y) + ((- (f * G)) + (- ((1 - f) * f))) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(f * Y),((- (f * G)) + (- ((1 - f) * f)))) is Element of the carrier of X

((f * Y) + ((- (f * G)) + (- ((1 - f) * f)))) + ((1 - f) * Y) is Element of the carrier of X

K179( the carrier of X, the U7 of X,((f * Y) + ((- (f * G)) + (- ((1 - f) * f)))),((1 - f) * Y)) is Element of the carrier of X

||.(((f * Y) + ((- (f * G)) + (- ((1 - f) * f)))) + ((1 - f) * Y)).|| is complex real ext-real non negative Element of REAL

(f * Y) + (- (f * G)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(f * Y),(- (f * G))) is Element of the carrier of X

((f * Y) + (- (f * G))) + (- ((1 - f) * f)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,((f * Y) + (- (f * G))),(- ((1 - f) * f))) is Element of the carrier of X

(((f * Y) + (- (f * G))) + (- ((1 - f) * f))) + ((1 - f) * Y) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(((f * Y) + (- (f * G))) + (- ((1 - f) * f))),((1 - f) * Y)) is Element of the carrier of X

||.((((f * Y) + (- (f * G))) + (- ((1 - f) * f))) + ((1 - f) * Y)).|| is complex real ext-real non negative Element of REAL

(f * Y) - (f * G) is Element of the carrier of X

K230(X,(f * Y),(- (f * G))) is Element of the carrier of X

((1 - f) * Y) - ((1 - f) * f) is Element of the carrier of X

K230(X,((1 - f) * Y),(- ((1 - f) * f))) is Element of the carrier of X

K179( the carrier of X, the U7 of X,((1 - f) * Y),(- ((1 - f) * f))) is Element of the carrier of X

((f * Y) - (f * G)) + (((1 - f) * Y) - ((1 - f) * f)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,((f * Y) - (f * G)),(((1 - f) * Y) - ((1 - f) * f))) is Element of the carrier of X

||.(((f * Y) - (f * G)) + (((1 - f) * Y) - ((1 - f) * f))).|| is complex real ext-real non negative Element of REAL

(f * (Y - G)) + (((1 - f) * Y) - ((1 - f) * f)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(f * (Y - G)),(((1 - f) * Y) - ((1 - f) * f))) is Element of the carrier of X

||.((f * (Y - G)) + (((1 - f) * Y) - ((1 - f) * f))).|| is complex real ext-real non negative Element of REAL

(f * (Y - G)) + ((1 - f) * (Y - f)) is Element of the carrier of X

K179( the carrier of X, the U7 of X,(f * (Y - G)),((1 - f) * (Y - f))) is Element of the carrier of X

||.((f * (Y - G)) + ((1 - f) * (Y - f))).|| is complex real ext-real non negative Element of REAL

f + (1 - f) is complex real ext-real Element of REAL

(f + (1 - f)) * Y is Element of the carrier of X

K175( the U9 of X,(f + (1 - f)),Y) is set

((f + (1 - f)) * Y) - ((f * G) + ((1 - f) * f)) is Element of the carrier of X

K230(X,((f + (1 - f)) * Y),(- ((f * G) + ((1 - f) * f)))) is Element of the carrier of X

K179( the carrier of X, the U7 of X,((f + (1 - f)) * Y),(- ((f * G) + ((1 - f) * f)))) is Element of the carrier of X

||.(((f + (1 - f)) * Y) - ((f * G) + ((1 - f) * f))).|| is complex real ext-real non negative Element of REAL

Y - ((f * G) + ((1 - f) * f)) is Element of the carrier of X

K230(X,Y,(- ((f * G) + ((1 - f) * f)))) is Element of the carrier of X

K179( the carrier of X, the U7 of X,Y,(- ((f * G) + ((1 - f) * f)))) is Element of the carrier of X

||.(Y - ((f * G) + ((1 - f) * f))).|| is complex real ext-real non negative Element of REAL

G is Element of the carrier of (LinearTopSpaceNorm X)

f is Element of the carrier of (LinearTopSpaceNorm X)

f is complex real ext-real Element of REAL

f * G is Element of the carrier of (LinearTopSpaceNorm X)

the U9 of (LinearTopSpaceNorm X) is V16() V19([:REAL, the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([:REAL, the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]

[:REAL, the carrier of (LinearTopSpaceNorm X):] is set