:: LOPBAN_6 semantic presentation

REAL is set

bool REAL is non empty set

bool omega is non empty set

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

bool is non empty set

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

bool is non empty 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

{} is set

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

(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) / (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) * T is complex real ext-real set

((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

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

(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

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

(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

Y / (1 + T) is complex real ext-real Element of REAL
F1() is non empty set
[:NAT,F1():] is non empty set
bool [:NAT,F1():] is non empty set
F2() is Element of F1()
F3() is Element of F1()
[:F1(),F1():] is non empty set

Y is Element of [:F1(),F1():]
Y `1 is set
Y `2 is set
Y `1 is Element of F1()
Y `2 is Element of F1()
TB1 is Element of F1()
G is Element of F1()
f is Element of F1()
[G,f] is V13() Element of [:F1(),F1():]
{G,f} is set
{G} is set
{{G,f},{G}} is set
n0 is Element of [:F1(),F1():]
n0 `2 is set
n0 `1 is set
[:NAT,[:F1(),F1():]:] is non empty set
bool [:NAT,[:F1(),F1():]:] is non empty set
[F2(),F3()] is V13() Element of [:F1(),F1():]
{F2(),F3()} is set
{F2()} is set
{{F2(),F3()},{F2()}} is set
X is non empty V16() V19( NAT ) V20([:F1(),F1():]) Function-like V26( NAT ) quasi_total Element of bool [:NAT,[:F1(),F1():]:]
X . 0 is Element of [:F1(),F1():]

X . Y is Element of [:F1(),F1():]
(X . Y) `1 is Element of F1()
Y is non empty V16() V19( NAT ) V20(F1()) Function-like V26( NAT ) quasi_total Element of bool [:NAT,F1():]

Y . T is Element of F1()
X . T is Element of [:F1(),F1():]
(X . T) `1 is Element of F1()

X . (T + 1) is Element of [:F1(),F1():]

X . ((T + 1) + 1) is Element of [:F1(),F1():]
(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

Y . (T + 2) is Element of F1()
(X . (T + 1)) `2 is Element of F1()
Y . (T + 1) is Element of F1()
(X . (T + 1)) `1 is Element of F1()
(X . T) `2 is Element of F1()
Y . 0 is Element of F1()
Y . 1 is Element of F1()

X . (0 + 1) is Element of [:F1(),F1():]
(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 F1()
X . 1 is Element of [:F1(),F1():]
(X . 1) `1 is Element of F1()

Y . T is Element of F1()

Y . (T + 1) is Element of F1()

Y . (T + 2) is Element of F1()
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

Ball (Y,T) 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 T <= ||.(Y - b1).|| } is set
Ball ((0. X),T) is Element of bool the carrier of X
{ b1 where b1 is Element of the carrier of X : not T <= ||.((0. X) - b1).|| } is set
Y + (Ball ((0. X),T)) is Element of bool the carrier of X
{ K230(X,Y,b1) where b1 is Element of the carrier of X : b1 in Ball ((0. X),T) } is set
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 + (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

Ball ((0. X),Y) 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 Y <= ||.((0. X) - b1).|| } is set

Ball ((0. X),(T * Y)) is Element of bool the carrier of X
{ b1 where b1 is Element of the carrier of X : not T * Y <= ||.((0. X) - b1).|| } is set
T * (Ball ((0. X),Y)) is Element of bool the carrier of X
{ (T * b1) where b1 is Element of the carrier of X : b1 in Ball ((0. X),Y) } is set
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

(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

(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 ")) * ||.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

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

- 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,b1,b2) where b1, b2 is Element of the carrier of X : ( b1 in T1 & b2 in TB1 ) } is set
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,b1,b2) where b1, b2 is Element of the carrier of Y : ( b1 in T .: T1 & b2 in T .: TB1 ) } is set
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 * T1 is Element of bool the carrier of X
{ (TB1 * b1) where b1 is Element of the carrier of X : b1 in T1 } is set
T .: (TB1 * T1) is Element of bool the carrier of Y
TB1 * (T .: T1) is Element of bool the carrier of Y
{ (TB1 * b1) where b1 is Element of the carrier of Y : b1 in T .: T1 } is set
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,b1) where b1 is Element of the carrier of X : b1 in T1 } is set
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),b1) where b1 is Element of the carrier of Y : b1 in T .: T1 } is set
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 is non empty set
bool the carrier of 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,b1,b2) where b1, b2 is Element of the carrier of X : ( b1 in Y & b2 in T ) } is set
T1 is Element of bool the carrier of
TB1 is Element of bool the carrier of
T1 + TB1 is Element of bool the carrier of
{ K230(,b1,b2) where b1, b2 is Element of the carrier of : ( b1 in T1 & b2 in TB1 ) } is set
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
n0 is Element of the carrier of
r + n0 is Element of the carrier of
the U7 of is non empty V16() V19([: the carrier of , the carrier of :]) V20( the carrier of ) Function-like V26([: the carrier of , the carrier of :]) quasi_total Element of bool [:[: the carrier of , the carrier of :], the carrier of :]
[: the carrier of , the carrier of :] is non empty set
[:[: the carrier of , the carrier of :], the carrier of :] is non empty set
bool [:[: the carrier of , the carrier of :], the carrier of :] is non empty set
K179( the carrier of , the U7 of ,r,n0) is Element of the carrier of
G is set
f is Element of the carrier of
f is Element of the carrier of
f + f is Element of the carrier of
the U7 of is non empty V16() V19([: the carrier of , the carrier of :]) V20( the carrier of ) Function-like V26([: the carrier of , the carrier of :]) quasi_total Element of bool [:[: the carrier of , the carrier of :], the carrier of :]
[: the carrier of , the carrier of :] is non empty set
[:[: the carrier of , the carrier of :], the carrier of :] is non empty set
bool [:[: the carrier of , the carrier of :], the carrier of :] is non empty set
K179( the carrier of , the U7 of ,f,f) is Element of the carrier of
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 is non empty set
bool the carrier of 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,b1) where b1 is Element of the carrier of X : b1 in Y } is set
T1 is Element of bool the carrier of
TB1 is Element of the carrier of
TB1 + T1 is Element of bool the carrier of
{ K230(,TB1,b1) where b1 is Element of the carrier of : b1 in T1 } is set
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
TB1 + f is Element of the carrier of
the U7 of is non empty V16() V19([: the carrier of , the carrier of :]) V20( the carrier of ) Function-like V26([: the carrier of , the carrier of :]) quasi_total Element of bool [:[: the carrier of , the carrier of :], the carrier of :]
[: the carrier of , the carrier of :] is non empty set
[:[: the carrier of , the carrier of :], the carrier of :] is non empty set
bool [:[: the carrier of , the carrier of :], the carrier of :] is non empty set
K179( the carrier of , the U7 of ,TB1,f) is Element of the carrier of
G is set
f is Element of the carrier of
TB1 + f is Element of the carrier of
the U7 of is non empty V16() V19([: the carrier of , the carrier of :]) V20( the carrier of ) Function-like V26([: the carrier of , the carrier of :]) quasi_total Element of bool [:[: the carrier of , the carrier of :], the carrier of :]
[: the carrier of , the carrier of :] is non empty set
[:[: the carrier of , the carrier of :], the carrier of :] is non empty set
bool [:[: the carrier of , the carrier of :], the carrier of :] is non empty set
K179( the carrier of , the U7 of ,TB1,f) is Element of the carrier of
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 is non empty set
bool the carrier of is non empty set
Y is Element of bool the carrier of X

T * Y is Element of bool the carrier of X
{ (T * b1) where b1 is Element of the carrier of X : b1 in Y } is set
T1 is Element of bool the carrier of
T * T1 is Element of bool the carrier of
{ (T * b1) where b1 is Element of the carrier of : b1 in T1 } is set
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
T * f is Element of the carrier of
the U9 of is V16() V19([:REAL, the carrier of :]) V20( the carrier of ) Function-like V26([:REAL, the carrier of :]) quasi_total Element of bool [:[:REAL, the carrier of :], the carrier of :]
[:REAL, the carrier of :] is set
[:[:REAL, the carrier of :], the carrier of :] is set
bool [:[:REAL, the carrier of :], the carrier of :] is non empty set
K175( the U9 of ,T,f) is set
TB1 is set
G is Element of the carrier of
T * G is Element of the carrier of
the U9 of is V16() V19([:REAL, the carrier of :]) V20( the carrier of ) Function-like V26([:REAL, the carrier of :]) quasi_total Element of bool [:[:REAL, the carrier of :], the carrier of :]
[:REAL, the carrier of :] is set
[:[:REAL, the carrier of :], the carrier of :] is set
bool [:[:REAL, the carrier of :], the carrier of :] is non empty set
K175( the U9 of ,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

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,) is V83() L7()
K210(()) is TopStruct
the carrier of () is non empty set
K209(()) is Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (),K209(()) #) is strict TopStruct
the carrier of () is non empty set
bool the carrier of () 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 is non empty set
bool the carrier of is non empty set
Y is Element of bool the carrier of ()
Cl Y is closed Element of bool the carrier of ()
T is Element of bool the carrier of
Cl T is closed Element of bool the carrier of
T1 is set
TB1 is Element of bool the carrier of
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 ()
T1 is set
TB1 is Element of bool the carrier of ()
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
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

Ball ((0. X),T) 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 T <= ||.((0. X) - b1).|| } is set
(- 1) * (Ball ((0. X),T)) is Element of bool the carrier of X
{ ((- 1) * b1) where b1 is Element of the carrier of X : b1 in Ball ((0. X),T) } is set
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

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 is non empty set
bool the carrier of is non empty set
Y is Element of the carrier of X

Ball (Y,T) 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 T <= ||.(Y - b1).|| } is set
T1 is Element of bool the carrier of
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 * 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) * 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) * 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

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) + ((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

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
f is Element of the carrier of

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