REAL is non empty V30() V176() V177() V178() V182() non bounded_below non bounded_above V197() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() left_end bounded_below Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V30() V176() V182() set
bool COMPLEX is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() left_end bounded_below set
bool omega is non empty set
bool NAT is non empty set
[:NAT,REAL:] is non empty V139() V140() V141() set
bool [:NAT,REAL:] is non empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() bounded_below V197() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real V101() ext-real positive non negative V176() V177() V178() V179() V180() V181() V187() left_end bounded_below Element of NAT
{{},1} is non empty V176() V177() V178() V179() V180() V181() left_end bounded_below set
RAT is non empty V30() V176() V177() V178() V179() V182() set
INT is non empty V30() V176() V177() V178() V179() V180() V182() set
[:COMPLEX,COMPLEX:] is non empty V139() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V139() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is non empty V139() V140() V141() set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty V139() V140() V141() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty RAT -valued V139() V140() V141() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty RAT -valued V139() V140() V141() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty RAT -valued INT -valued V139() V140() V141() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty RAT -valued INT -valued V139() V140() V141() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty RAT -valued INT -valued V139() V140() V141() V142() set
[:[:NAT,NAT:],NAT:] is non empty RAT -valued INT -valued V139() V140() V141() V142() set
bool [:[:NAT,NAT:],NAT:] is non empty set
[:COMPLEX,REAL:] is non empty V139() V140() V141() set
bool [:COMPLEX,REAL:] is non empty set
ExtREAL is non empty V177() V197() set
[:NAT,COMPLEX:] is non empty V139() set
bool [:NAT,COMPLEX:] is non empty set
K568() is non empty set
[:K568(),K568():] is non empty set
[:[:K568(),K568():],K568():] is non empty set
bool [:[:K568(),K568():],K568():] is non empty set
[:COMPLEX,K568():] is non empty set
[:[:COMPLEX,K568():],K568():] is non empty set
bool [:[:COMPLEX,K568():],K568():] is non empty set
K574() is non empty strict CLSStruct
the carrier of K574() is non empty set
bool the carrier of K574() is non empty set
K578() is Element of bool the carrier of K574()
[:K578(),K578():] is set
[:[:K578(),K578():],COMPLEX:] is V139() set
bool [:[:K578(),K578():],COMPLEX:] is non empty set
K586() is Element of bool the carrier of K574()
[:K586(),REAL:] is V139() V140() V141() set
bool [:K586(),REAL:] is non empty set
[:1,1:] is non empty RAT -valued INT -valued V139() V140() V141() V142() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty RAT -valued INT -valued V139() V140() V141() V142() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty V139() V140() V141() set
bool [:[:1,1:],REAL:] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real V101() ext-real positive non negative V176() V177() V178() V179() V180() V181() V187() left_end bounded_below Element of NAT
[:2,2:] is non empty RAT -valued INT -valued V139() V140() V141() V142() set
[:[:2,2:],REAL:] is non empty V139() V140() V141() set
bool [:[:2,2:],REAL:] is non empty set
K760() is TopStruct
the carrier of K760() is set
K714() is V258() L25()
K765() is TopSpace-like TopStruct
the carrier of K765() is set
K800(2) is V294() L26()
the carrier of K800(2) is set
[: the carrier of K800(2),REAL:] is V139() V140() V141() set
bool [: the carrier of K800(2),REAL:] is non empty set
bool the carrier of K800(2) is non empty set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() bounded_below V197() Element of NAT
1r is complex Element of COMPLEX
- 1r is complex Element of COMPLEX
X is TopStruct
the carrier of X is set
[: the carrier of X,COMPLEX:] is V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
X is 1-sorted
the carrier of X is set
X is complex set
the carrier of X --> X is Relation-like the carrier of X -defined {X} -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,{X}:]
{X} is non empty V176() set
[: the carrier of X,{X}:] is V139() set
bool [: the carrier of X,{X}:] is non empty set
[: the carrier of X,COMPLEX:] is V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of X,COMPLEX:] is non empty V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
X is complex set
(X,X) is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
the carrier of X --> X is non empty Relation-like the carrier of X -defined {X} -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,{X}:]
{X} is non empty V176() set
[: the carrier of X,{X}:] is non empty V139() set
bool [: the carrier of X,{X}:] is non empty set
F is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
[#] X is non empty non proper closed Element of bool the carrier of X
bool the carrier of X is non empty set
GB is V176() Element of bool COMPLEX
F " GB is Element of bool the carrier of X
{} X is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() bounded_below V197() closed compact Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
X is complex set
(X,X) is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
the carrier of X is non empty set
[: the carrier of X,COMPLEX:] is non empty V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
the carrier of X --> X is non empty Relation-like the carrier of X -defined {X} -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,{X}:]
{X} is non empty V176() set
[: the carrier of X,{X}:] is non empty V139() set
bool [: the carrier of X,{X}:] is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of X,COMPLEX:] is non empty V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
0c is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() bounded_below V197() Element of COMPLEX
(X,0c) is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
the carrier of X --> 0c is non empty Relation-like the carrier of X -defined {0c} -valued Function-like total quasi_total V139() V140() V141() V142() Element of bool [: the carrier of X,{0c}:]
{0c} is non empty V176() V177() V178() V179() V180() V181() left_end bounded_below set
[: the carrier of X,{0c}:] is non empty RAT -valued INT -valued V139() V140() V141() V142() set
bool [: the carrier of X,{0c}:] is non empty set
X is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of X,COMPLEX:] is non empty V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
X is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
F is V176() Element of bool COMPLEX
F ` is V176() Element of bool COMPLEX
COMPLEX \ F is V176() set
X " (F `) is Element of bool the carrier of X
bool the carrier of X is non empty set
X " COMPLEX is Element of bool the carrier of X
X " F is Element of bool the carrier of X
(X " COMPLEX) \ (X " F) is Element of bool the carrier of X
[#] X is non empty non proper closed Element of bool the carrier of X
([#] X) \ (X " F) is Element of bool the carrier of X
([#] X) \ (([#] X) \ (X " F)) is Element of bool the carrier of X
F is V176() Element of bool COMPLEX
X " F is Element of bool the carrier of X
F ` is V176() Element of bool COMPLEX
COMPLEX \ F is V176() set
(F `) ` is V176() Element of bool COMPLEX
COMPLEX \ (F `) is V176() set
X " (F `) is Element of bool the carrier of X
(X " COMPLEX) \ (X " F) is Element of bool the carrier of X
([#] X) \ (X " F) is Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of X,COMPLEX:] is non empty V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
bool the carrier of X is non empty set
X is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
F is Element of the carrier of X
X . F is complex Element of COMPLEX
G is V176() Element of bool COMPLEX
GB is complex set
aFB is V176() Neighbourhood of GB
aF is complex real ext-real Element of REAL
{ b1 where b1 is complex set : not aF <= |.(b1 - GB).| } is set
r is set
r is complex set
r - GB is complex set
- GB is complex set
r + (- GB) is complex set
|.(r - GB).| is complex real ext-real non negative Element of REAL
X " { b1 where b1 is complex set : not aF <= |.(b1 - GB).| } is Element of bool the carrier of X
r is V176() Element of bool COMPLEX
r is Element of bool the carrier of X
X .: (X " { b1 where b1 is complex set : not aF <= |.(b1 - GB).| } ) is V176() Element of bool COMPLEX
X .: r is V176() Element of bool COMPLEX
F is Element of the carrier of X
X . F is complex Element of COMPLEX
G is V176() Element of bool COMPLEX
F is V176() Element of bool COMPLEX
F ` is V176() Element of bool COMPLEX
COMPLEX \ F is V176() set
(F `) ` is V176() Element of bool COMPLEX
COMPLEX \ (F `) is V176() set
X " F is Element of bool the carrier of X
(X " F) ` is Element of bool the carrier of X
the carrier of X \ (X " F) is set
G is Element of the carrier of X
X " (F `) is Element of bool the carrier of X
X . G is complex Element of COMPLEX
FB is V176() Element of bool COMPLEX
GB is Element of bool the carrier of X
X .: GB is V176() Element of bool COMPLEX
X " (X .: GB) is Element of bool the carrier of X
((X " F) `) ` is Element of bool the carrier of X
the carrier of X \ ((X " F) `) is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of X,COMPLEX:] is non empty V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
X is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
F is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
X + F is Relation-like the carrier of X -defined Function-like total V139() set
rng (X + F) is V176() set
dom (X + F) is Element of bool the carrier of X
bool the carrier of X is non empty set
dom X is Element of bool the carrier of X
dom F is Element of bool the carrier of X
(dom X) /\ (dom F) is Element of bool the carrier of X
the carrier of X /\ (dom F) is Element of bool the carrier of X
the carrier of X /\ the carrier of X is set
FB is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
GB is Element of the carrier of X
FB . GB is complex Element of COMPLEX
X . GB is complex Element of COMPLEX
F . GB is complex Element of COMPLEX
(X . GB) + (F . GB) is complex Element of COMPLEX
GB is Element of the carrier of X
FB . GB is complex Element of COMPLEX
aFB is V176() Element of bool COMPLEX
aF is complex set
aG is V176() Neighbourhood of aF
r is complex real ext-real Element of REAL
{ b1 where b1 is complex set : not r <= |.(b1 - aF).| } is set
r / 2 is complex real ext-real Element of COMPLEX
2 " is non empty complex real ext-real positive non negative set
r * (2 ") is complex real ext-real set
X . GB is complex Element of COMPLEX
s1 is complex set
{ b1 where b1 is complex set : not r / 2 <= |.(b1 - s1).| } is set
A2 is set
A3 is complex set
A3 - s1 is complex set
- s1 is complex set
A3 + (- s1) is complex set
|.(A3 - s1).| is complex real ext-real non negative Element of REAL
A2 is V176() Element of bool COMPLEX
s1 - s1 is complex set
- s1 is complex set
s1 + (- s1) is complex set
|.(s1 - s1).| is complex real ext-real non negative Element of REAL
A3 is Element of bool the carrier of X
X .: A3 is V176() Element of bool COMPLEX
F . GB is complex Element of COMPLEX
vv1 is complex set
{ b1 where b1 is complex set : not r / 2 <= |.(b1 - vv1).| } is set
fvu1 is set
zz0 is complex set
zz0 - vv1 is complex set
- vv1 is complex set
zz0 + (- vv1) is complex set
|.(zz0 - vv1).| is complex real ext-real non negative Element of REAL
fvu1 is V176() Element of bool COMPLEX
vv1 - vv1 is complex set
- vv1 is complex set
vv1 + (- vv1) is complex set
|.(vv1 - vv1).| is complex real ext-real non negative Element of REAL
zz0 is Element of bool the carrier of X
F .: zz0 is V176() Element of bool COMPLEX
A3 /\ zz0 is Element of bool the carrier of X
FB .: (A3 /\ zz0) is V176() Element of bool COMPLEX
hx0 is set
dom FB is Element of bool the carrier of X
W3 is set
FB . W3 is complex set
W is Element of the carrier of X
X . W is complex Element of COMPLEX
F . W is complex Element of COMPLEX
x3 is complex set
x3 - vv1 is complex set
x3 + (- vv1) is complex set
|.(x3 - vv1).| is complex real ext-real non negative Element of REAL
px is complex set
px - vv1 is complex set
px + (- vv1) is complex set
|.(px - vv1).| is complex real ext-real non negative Element of REAL
(FB . W3) - aF is complex set
- aF is complex set
(FB . W3) + (- aF) is complex set
|.((FB . W3) - aF).| is complex real ext-real non negative Element of REAL
(X . W) + (F . W) is complex Element of COMPLEX
((X . W) + (F . W)) - aF is complex set
((X . W) + (F . W)) + (- aF) is complex set
|.(((X . W) + (F . W)) - aF).| is complex real ext-real non negative Element of REAL
(X . GB) + (F . GB) is complex Element of COMPLEX
((X . W) + (F . W)) - ((X . GB) + (F . GB)) is complex Element of COMPLEX
- ((X . GB) + (F . GB)) is complex set
((X . W) + (F . W)) + (- ((X . GB) + (F . GB))) is complex set
|.(((X . W) + (F . W)) - ((X . GB) + (F . GB))).| is complex real ext-real non negative Element of REAL
z3 is complex set
z3 - s1 is complex set
z3 + (- s1) is complex set
(z3 - s1) + (x3 - vv1) is complex set
|.((z3 - s1) + (x3 - vv1)).| is complex real ext-real non negative Element of REAL
FB . W is complex Element of COMPLEX
(FB . W) - aF is complex set
(FB . W) + (- aF) is complex set
|.((FB . W) - aF).| is complex real ext-real non negative Element of REAL
|.(z3 - s1).| is complex real ext-real non negative Element of REAL
|.(z3 - s1).| + |.(x3 - vv1).| is complex real ext-real non negative Element of REAL
(r / 2) + |.(x3 - vv1).| is complex real ext-real Element of REAL
px is complex set
px - s1 is complex set
px + (- s1) is complex set
|.(px - s1).| is complex real ext-real non negative Element of REAL
(r / 2) + (r / 2) is complex real ext-real Element of COMPLEX
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of X,COMPLEX:] is non empty V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
X is complex set
F is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
X (#) F is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
FB is Element of the carrier of X
(X (#) F) . FB is complex Element of COMPLEX
F . FB is complex Element of COMPLEX
X * (F . FB) is complex set
bool the carrier of X is non empty set
FB is Element of the carrier of X
(X (#) F) . FB is complex Element of COMPLEX
GB is V176() Element of bool COMPLEX
aFB is complex set
aF is V176() Neighbourhood of aFB
aG is complex real ext-real Element of REAL
{ b1 where b1 is complex set : not aG <= |.(b1 - aFB).| } is set
|.X.| is complex real ext-real non negative Element of REAL
aG / |.X.| is complex real ext-real Element of COMPLEX
|.X.| " is complex real ext-real non negative set
aG * (|.X.| ") is complex real ext-real set
F . FB is complex Element of COMPLEX
r is complex set
{ b1 where b1 is complex set : not aG / |.X.| <= |.(b1 - r).| } is set
fau1 is set
A2 is complex set
A2 - r is complex set
- r is complex set
A2 + (- r) is complex set
|.(A2 - r).| is complex real ext-real non negative Element of REAL
fau1 is V176() Element of bool COMPLEX
r - r is complex set
- r is complex set
r + (- r) is complex set
|.(r - r).| is complex real ext-real non negative Element of REAL
A2 is Element of bool the carrier of X
F .: A2 is V176() Element of bool COMPLEX
(X (#) F) .: A2 is V176() Element of bool COMPLEX
vv1 is set
dom (X (#) F) is Element of bool the carrier of X
uu1 is set
(X (#) F) . uu1 is complex set
fvu1 is Element of the carrier of X
dom F is Element of bool the carrier of X
F . fvu1 is complex Element of COMPLEX
zz0 is complex set
zz0 - r is complex set
zz0 + (- r) is complex set
|.(zz0 - r).| is complex real ext-real non negative Element of REAL
xx0 is complex set
xx0 - r is complex set
xx0 + (- r) is complex set
|.(xx0 - r).| is complex real ext-real non negative Element of REAL
((X (#) F) . uu1) - aFB is complex set
- aFB is complex set
((X (#) F) . uu1) + (- aFB) is complex set
|.(((X (#) F) . uu1) - aFB).| is complex real ext-real non negative Element of REAL
X * (F . fvu1) is complex set
(X * (F . fvu1)) - aFB is complex set
(X * (F . fvu1)) + (- aFB) is complex set
|.((X * (F . fvu1)) - aFB).| is complex real ext-real non negative Element of REAL
X * (F . FB) is complex set
(X * (F . fvu1)) - (X * (F . FB)) is complex set
- (X * (F . FB)) is complex set
(X * (F . fvu1)) + (- (X * (F . FB))) is complex set
|.((X * (F . fvu1)) - (X * (F . FB))).| is complex real ext-real non negative Element of REAL
(F . fvu1) - (F . FB) is complex Element of COMPLEX
- (F . FB) is complex set
(F . fvu1) + (- (F . FB)) is complex set
X * ((F . fvu1) - (F . FB)) is complex set
|.(X * ((F . fvu1) - (F . FB))).| is complex real ext-real non negative Element of REAL
|.X.| * |.(zz0 - r).| is complex real ext-real non negative Element of REAL
|.X.| * (aG / |.X.|) is complex real ext-real Element of REAL
|.X.| / |.X.| is complex real ext-real non negative Element of COMPLEX
|.X.| * (|.X.| ") is complex real ext-real non negative set
aG * (|.X.| / |.X.|) is complex real ext-real Element of REAL
aG * 1 is complex real ext-real Element of REAL
(X (#) F) . fvu1 is complex Element of COMPLEX
((X (#) F) . fvu1) - aFB is complex set
((X (#) F) . fvu1) + (- aFB) is complex set
|.(((X (#) F) . fvu1) - aFB).| is complex real ext-real non negative Element of REAL
0c is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() bounded_below V197() Element of COMPLEX
(X,0c) is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
the carrier of X --> 0c is non empty Relation-like the carrier of X -defined {0c} -valued Function-like total quasi_total V139() V140() V141() V142() Element of bool [: the carrier of X,{0c}:]
{0c} is non empty V176() V177() V178() V179() V180() V181() left_end bounded_below set
[: the carrier of X,{0c}:] is non empty RAT -valued INT -valued V139() V140() V141() V142() set
bool [: the carrier of X,{0c}:] is non empty set
dom (X,0c) is Element of bool the carrier of X
bool the carrier of X is non empty set
dom (X (#) F) is Element of bool the carrier of X
aFB is set
(X,0c) . aFB is complex set
(X (#) F) . aFB is complex set
F . aFB is complex set
0 * (F . aFB) is complex set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of X,COMPLEX:] is non empty V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
X is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
F is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
X - F is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
- F is Relation-like the carrier of X -defined Function-like total V139() set
- 1 is non empty complex real ext-real non positive negative set
(- 1) (#) F is Relation-like the carrier of X -defined Function-like total V139() set
X + (- F) is Relation-like the carrier of X -defined Function-like total V139() set
- 1 is non empty complex real ext-real non positive negative Element of REAL
(- 1) (#) F is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of X,COMPLEX:] is non empty V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
X is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
F is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
X (#) F is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
FB is Element of the carrier of X
(X (#) F) . FB is complex Element of COMPLEX
X . FB is complex Element of COMPLEX
F . FB is complex Element of COMPLEX
(X . FB) * (F . FB) is complex Element of COMPLEX
bool the carrier of X is non empty set
FB is Element of the carrier of X
(X (#) F) . FB is complex Element of COMPLEX
GB is V176() Element of bool COMPLEX
aFB is complex set
aF is V176() Neighbourhood of aFB
aG is complex real ext-real Element of REAL
{ b1 where b1 is complex set : not aG <= |.(b1 - aFB).| } is set
X . FB is complex Element of COMPLEX
F . FB is complex Element of COMPLEX
r is complex set
|.r.| is complex real ext-real non negative Element of REAL
s1 is complex set
|.s1.| is complex real ext-real non negative Element of REAL
|.r.| + |.s1.| is complex real ext-real non negative Element of REAL
(|.r.| + |.s1.|) + 1 is non empty complex real ext-real positive non negative Element of REAL
aG / ((|.r.| + |.s1.|) + 1) is complex real ext-real Element of COMPLEX
((|.r.| + |.s1.|) + 1) " is non empty complex real ext-real positive non negative set
aG * (((|.r.| + |.s1.|) + 1) ") is complex real ext-real set
{ b1 where b1 is complex set : not aG / ((|.r.| + |.s1.|) + 1) <= |.(b1 - r).| } is set
A3 is set
vv1 is complex set
vv1 - r is complex set
- r is complex set
vv1 + (- r) is complex set
|.(vv1 - r).| is complex real ext-real non negative Element of REAL
A3 is V176() Element of bool COMPLEX
r - r is complex set
- r is complex set
r + (- r) is complex set
|.(r - r).| is complex real ext-real non negative Element of REAL
vv1 is Element of bool the carrier of X
X .: vv1 is V176() Element of bool COMPLEX
{ b1 where b1 is complex set : not aG / ((|.r.| + |.s1.|) + 1) <= |.(b1 - s1).| } is set
fvu1 is set
zz0 is complex set
zz0 - s1 is complex set
- s1 is complex set
zz0 + (- s1) is complex set
|.(zz0 - s1).| is complex real ext-real non negative Element of REAL
fvu1 is V176() Element of bool COMPLEX
s1 - s1 is complex set
- s1 is complex set
s1 + (- s1) is complex set
|.(s1 - s1).| is complex real ext-real non negative Element of REAL
zz0 is Element of bool the carrier of X
F .: zz0 is V176() Element of bool COMPLEX
{ b1 where b1 is complex set : not 1 <= |.(b1 - r).| } is set
hx0 is set
W3 is complex set
W3 - r is complex set
W3 + (- r) is complex set
|.(W3 - r).| is complex real ext-real non negative Element of REAL
hx0 is V176() Element of bool COMPLEX
W3 is Element of bool the carrier of X
X .: W3 is V176() Element of bool COMPLEX
vv1 /\ zz0 is Element of bool the carrier of X
(vv1 /\ zz0) /\ W3 is Element of bool the carrier of X
(X (#) F) .: ((vv1 /\ zz0) /\ W3) is V176() Element of bool COMPLEX
z3 is set
dom (X (#) F) is Element of bool the carrier of X
x3 is set
(X (#) F) . x3 is complex set
px is Element of the carrier of X
dom X is Element of bool the carrier of X
X . px is complex Element of COMPLEX
a1 is complex set
a1 - r is complex set
a1 + (- r) is complex set
|.(a1 - r).| is complex real ext-real non negative Element of REAL
a2 is complex set
a2 - r is complex set
a2 + (- r) is complex set
|.(a2 - r).| is complex real ext-real non negative Element of REAL
dom F is Element of bool the carrier of X
F . px is complex Element of COMPLEX
a2 is complex set
a2 - s1 is complex set
a2 + (- s1) is complex set
|.(a2 - s1).| is complex real ext-real non negative Element of REAL
a3 is complex set
a3 - s1 is complex set
a3 + (- s1) is complex set
|.(a3 - s1).| is complex real ext-real non negative Element of REAL
a3 is complex set
a3 - r is complex set
a3 + (- r) is complex set
|.(a3 - r).| is complex real ext-real non negative Element of REAL
c30 is complex set
c30 - r is complex set
c30 + (- r) is complex set
|.(c30 - r).| is complex real ext-real non negative Element of REAL
(a1 - r) + r is complex set
|.((a1 - r) + r).| is complex real ext-real non negative Element of REAL
|.(a1 - r).| + |.r.| is complex real ext-real non negative Element of REAL
|.a1.| is complex real ext-real non negative Element of REAL
|.a1.| - |.r.| is complex real ext-real Element of REAL
- |.r.| is complex real ext-real non positive set
|.a1.| + (- |.r.|) is complex real ext-real set
(|.(a1 - r).| + |.r.|) - |.r.| is complex real ext-real Element of REAL
(|.(a1 - r).| + |.r.|) + (- |.r.|) is complex real ext-real set
1 + |.r.| is non empty complex real ext-real positive non negative Element of REAL
(|.a1.| - |.r.|) + |.r.| is complex real ext-real Element of REAL
((X (#) F) . x3) - aFB is complex set
- aFB is complex set
((X (#) F) . x3) + (- aFB) is complex set
|.(((X (#) F) . x3) - aFB).| is complex real ext-real non negative Element of REAL
(X . px) * (F . px) is complex Element of COMPLEX
((X . px) * (F . px)) - aFB is complex set
((X . px) * (F . px)) + (- aFB) is complex set
|.(((X . px) * (F . px)) - aFB).| is complex real ext-real non negative Element of REAL
a1 * a2 is complex set
r * s1 is complex set
(a1 * a2) - (r * s1) is complex set
- (r * s1) is complex set
(a1 * a2) + (- (r * s1)) is complex set
|.((a1 * a2) - (r * s1)).| is complex real ext-real non negative Element of REAL
a1 * s1 is complex set
(a1 * a2) - (a1 * s1) is complex set
- (a1 * s1) is complex set
(a1 * a2) + (- (a1 * s1)) is complex set
(a1 * s1) - (r * s1) is complex set
(a1 * s1) + (- (r * s1)) is complex set
((a1 * a2) - (a1 * s1)) + ((a1 * s1) - (r * s1)) is complex set
|.(((a1 * a2) - (a1 * s1)) + ((a1 * s1) - (r * s1))).| is complex real ext-real non negative Element of REAL
|.((a1 * a2) - (a1 * s1)).| is complex real ext-real non negative Element of REAL
|.((a1 * s1) - (r * s1)).| is complex real ext-real non negative Element of REAL
|.((a1 * a2) - (a1 * s1)).| + |.((a1 * s1) - (r * s1)).| is complex real ext-real non negative Element of REAL
a1 * (a2 - s1) is complex set
|.(a1 * (a2 - s1)).| is complex real ext-real non negative Element of REAL
s1 * (a1 - r) is complex set
|.(s1 * (a1 - r)).| is complex real ext-real non negative Element of REAL
|.(a1 * (a2 - s1)).| + |.(s1 * (a1 - r)).| is complex real ext-real non negative Element of REAL
|.a1.| * |.(a2 - s1).| is complex real ext-real non negative Element of REAL
(|.a1.| * |.(a2 - s1).|) + |.(s1 * (a1 - r)).| is complex real ext-real non negative Element of REAL
|.s1.| * |.(a1 - r).| is complex real ext-real non negative Element of REAL
(|.a1.| * |.(a2 - s1).|) + (|.s1.| * |.(a1 - r).|) is complex real ext-real non negative Element of REAL
|.a1.| * (aG / ((|.r.| + |.s1.|) + 1)) is complex real ext-real Element of REAL
(1 + |.r.|) * (aG / ((|.r.| + |.s1.|) + 1)) is complex real ext-real Element of REAL
|.s1.| * (aG / ((|.r.| + |.s1.|) + 1)) is complex real ext-real Element of REAL
((1 + |.r.|) * (aG / ((|.r.| + |.s1.|) + 1))) + (|.s1.| * |.(a1 - r).|) is complex real ext-real Element of REAL
((1 + |.r.|) * (aG / ((|.r.| + |.s1.|) + 1))) + (|.s1.| * (aG / ((|.r.| + |.s1.|) + 1))) is complex real ext-real Element of REAL
((|.r.| + |.s1.|) + 1) / ((|.r.| + |.s1.|) + 1) is non empty complex real ext-real positive non negative Element of COMPLEX
((|.r.| + |.s1.|) + 1) * (((|.r.| + |.s1.|) + 1) ") is non empty complex real ext-real positive non negative set
aG * (((|.r.| + |.s1.|) + 1) / ((|.r.| + |.s1.|) + 1)) is complex real ext-real Element of REAL
(X (#) F) . px is complex Element of COMPLEX
((X (#) F) . px) - aFB is complex set
((X (#) F) . px) + (- aFB) is complex set
|.(((X (#) F) . px) - aFB).| is complex real ext-real non negative Element of REAL
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of X,COMPLEX:] is non empty V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
[: the carrier of X,REAL:] is non empty V139() V140() V141() set
bool [: the carrier of X,REAL:] is non empty set
X is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
|.X.| is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V139() V140() V141() Element of bool [: the carrier of X,REAL:]
F is non empty Relation-like the carrier of X -defined REAL -valued Function-like total quasi_total V139() V140() V141() Element of bool [: the carrier of X,REAL:]
bool the carrier of X is non empty set
G is Element of the carrier of X
F . G is complex real ext-real Element of REAL
FB is V176() V177() V178() Element of bool REAL
GB is complex real ext-real Element of REAL
aFB is complex real ext-real set
GB - aFB is complex real ext-real Element of REAL
- aFB is complex real ext-real set
GB + (- aFB) is complex real ext-real set
GB + aFB is complex real ext-real Element of REAL
].(GB - aFB),(GB + aFB).[ is V176() V177() V178() non left_end non right_end V197() Element of bool REAL
X . G is complex Element of COMPLEX
aG is complex set
{ b1 where b1 is complex set : not aFB <= |.(b1 - aG).| } is set
r is set
s1 is complex set
s1 - aG is complex set
- aG is complex set
s1 + (- aG) is complex set
|.(s1 - aG).| is complex real ext-real non negative Element of REAL
r is V176() Element of bool COMPLEX
aG - aG is complex set
- aG is complex set
aG + (- aG) is complex set
|.(aG - aG).| is complex real ext-real non negative Element of REAL
s1 is Element of bool the carrier of X
X .: s1 is V176() Element of bool COMPLEX
F .: s1 is V176() V177() V178() Element of bool REAL
A2 is set
dom F is Element of bool the carrier of X
A3 is set
F . A3 is complex real ext-real set
vv1 is Element of the carrier of X
dom X is Element of bool the carrier of X
X . vv1 is complex Element of COMPLEX
uu1 is complex set
uu1 - aG is complex set
uu1 + (- aG) is complex set
|.(uu1 - aG).| is complex real ext-real non negative Element of REAL
fvu1 is complex set
fvu1 - aG is complex set
fvu1 + (- aG) is complex set
|.(fvu1 - aG).| is complex real ext-real non negative Element of REAL
(F . A3) - GB is complex real ext-real Element of REAL
- GB is complex real ext-real set
(F . A3) + (- GB) is complex real ext-real set
|.((F . A3) - GB).| is complex real ext-real non negative Element of REAL
|.(X . vv1).| is complex real ext-real non negative Element of REAL
|.X.| . G is complex real ext-real Element of REAL
|.(X . vv1).| - (|.X.| . G) is complex real ext-real Element of REAL
- (|.X.| . G) is complex real ext-real set
|.(X . vv1).| + (- (|.X.| . G)) is complex real ext-real set
|.(|.(X . vv1).| - (|.X.| . G)).| is complex real ext-real non negative Element of REAL
|.(X . G).| is complex real ext-real non negative Element of REAL
|.(X . vv1).| - |.(X . G).| is complex real ext-real Element of REAL
- |.(X . G).| is complex real ext-real non positive set
|.(X . vv1).| + (- |.(X . G).|) is complex real ext-real set
|.(|.(X . vv1).| - |.(X . G).|).| is complex real ext-real non negative Element of REAL
(X . vv1) - (X . G) is complex Element of COMPLEX
- (X . G) is complex set
(X . vv1) + (- (X . G)) is complex set
|.((X . vv1) - (X . G)).| is complex real ext-real non negative Element of REAL
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of X,COMPLEX:] is non empty V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
{ b1 where b1 is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:] : verum } is set
CAlgebra the carrier of X is non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital strict vector-associative ComplexAlgebraStr
Funcs ( the carrier of X,COMPLEX) is non empty functional FUNCTION_DOMAIN of the carrier of X, COMPLEX
ComplexFuncMult the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):] -defined Funcs ( the carrier of X,COMPLEX) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):]
[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):] is non empty set
[:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
bool [:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
ComplexFuncAdd the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):] -defined Funcs ( the carrier of X,COMPLEX) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):]
ComplexFuncExtMult the carrier of X is non empty Relation-like [:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):] -defined Funcs ( the carrier of X,COMPLEX) -valued Function-like total quasi_total Element of bool [:[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):]
[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):] is non empty set
[:[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
bool [:[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
ComplexFuncUnit the carrier of X is Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs ( the carrier of X,COMPLEX)
the carrier of X --> 1r is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
ComplexFuncZero the carrier of X is Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs ( the carrier of X,COMPLEX)
the carrier of X --> 0 is non empty Relation-like the carrier of X -defined REAL -valued RAT -valued INT -valued Function-like total quasi_total V139() V140() V141() V142() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty V139() V140() V141() set
bool [: the carrier of X,REAL:] is non empty set
ComplexAlgebraStr(# (Funcs ( the carrier of X,COMPLEX)),(ComplexFuncMult the carrier of X),(ComplexFuncAdd the carrier of X),(ComplexFuncExtMult the carrier of X),(ComplexFuncUnit the carrier of X),(ComplexFuncZero the carrier of X) #) is strict ComplexAlgebraStr
the carrier of (CAlgebra the carrier of X) is non empty set
bool the carrier of (CAlgebra the carrier of X) is non empty set
F is set
G is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
X is non empty TopSpace-like TopStruct
(X) is Element of bool the carrier of (CAlgebra the carrier of X)
the carrier of X is non empty set
CAlgebra the carrier of X is non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital strict vector-associative ComplexAlgebraStr
Funcs ( the carrier of X,COMPLEX) is non empty functional FUNCTION_DOMAIN of the carrier of X, COMPLEX
ComplexFuncMult the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):] -defined Funcs ( the carrier of X,COMPLEX) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):]
[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):] is non empty set
[:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
bool [:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
ComplexFuncAdd the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):] -defined Funcs ( the carrier of X,COMPLEX) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):]
ComplexFuncExtMult the carrier of X is non empty Relation-like [:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):] -defined Funcs ( the carrier of X,COMPLEX) -valued Function-like total quasi_total Element of bool [:[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):]
[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):] is non empty set
[:[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
bool [:[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
ComplexFuncUnit the carrier of X is Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs ( the carrier of X,COMPLEX)
the carrier of X --> 1r is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
[: the carrier of X,COMPLEX:] is non empty V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
ComplexFuncZero the carrier of X is Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs ( the carrier of X,COMPLEX)
the carrier of X --> 0 is non empty Relation-like the carrier of X -defined REAL -valued RAT -valued INT -valued Function-like total quasi_total V139() V140() V141() V142() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty V139() V140() V141() set
bool [: the carrier of X,REAL:] is non empty set
ComplexAlgebraStr(# (Funcs ( the carrier of X,COMPLEX)),(ComplexFuncMult the carrier of X),(ComplexFuncAdd the carrier of X),(ComplexFuncExtMult the carrier of X),(ComplexFuncUnit the carrier of X),(ComplexFuncZero the carrier of X) #) is strict ComplexAlgebraStr
the carrier of (CAlgebra the carrier of X) is non empty set
bool the carrier of (CAlgebra the carrier of X) is non empty set
{ b1 where b1 is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:] : verum } is set
0c is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() bounded_below V197() Element of COMPLEX
(X,0c) is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
the carrier of X --> 0c is non empty Relation-like the carrier of X -defined {0c} -valued Function-like total quasi_total V139() V140() V141() V142() Element of bool [: the carrier of X,{0c}:]
{0c} is non empty V176() V177() V178() V179() V180() V181() left_end bounded_below set
[: the carrier of X,{0c}:] is non empty RAT -valued INT -valued V139() V140() V141() V142() set
bool [: the carrier of X,{0c}:] is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
CAlgebra the carrier of X is non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital strict vector-associative ComplexAlgebraStr
Funcs ( the carrier of X,COMPLEX) is non empty functional FUNCTION_DOMAIN of the carrier of X, COMPLEX
ComplexFuncMult the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):] -defined Funcs ( the carrier of X,COMPLEX) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):]
[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):] is non empty set
[:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
bool [:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
ComplexFuncAdd the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):] -defined Funcs ( the carrier of X,COMPLEX) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):]
ComplexFuncExtMult the carrier of X is non empty Relation-like [:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):] -defined Funcs ( the carrier of X,COMPLEX) -valued Function-like total quasi_total Element of bool [:[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):]
[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):] is non empty set
[:[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
bool [:[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
ComplexFuncUnit the carrier of X is Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs ( the carrier of X,COMPLEX)
the carrier of X --> 1r is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
[: the carrier of X,COMPLEX:] is non empty V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
ComplexFuncZero the carrier of X is Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs ( the carrier of X,COMPLEX)
the carrier of X --> 0 is non empty Relation-like the carrier of X -defined REAL -valued RAT -valued INT -valued Function-like total quasi_total V139() V140() V141() V142() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty V139() V140() V141() set
bool [: the carrier of X,REAL:] is non empty set
ComplexAlgebraStr(# (Funcs ( the carrier of X,COMPLEX)),(ComplexFuncMult the carrier of X),(ComplexFuncAdd the carrier of X),(ComplexFuncExtMult the carrier of X),(ComplexFuncUnit the carrier of X),(ComplexFuncZero the carrier of X) #) is strict ComplexAlgebraStr
(X) is non empty Element of bool the carrier of (CAlgebra the carrier of X)
the carrier of (CAlgebra the carrier of X) is non empty set
bool the carrier of (CAlgebra the carrier of X) is non empty set
{ b1 where b1 is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:] : verum } is set
G is Element of the carrier of (CAlgebra the carrier of X)
FB is Element of the carrier of (CAlgebra the carrier of X)
G + FB is Element of the carrier of (CAlgebra the carrier of X)
the addF of (CAlgebra the carrier of X) is non empty Relation-like [: the carrier of (CAlgebra the carrier of X), the carrier of (CAlgebra the carrier of X):] -defined the carrier of (CAlgebra the carrier of X) -valued Function-like total quasi_total Element of bool [:[: the carrier of (CAlgebra the carrier of X), the carrier of (CAlgebra the carrier of X):], the carrier of (CAlgebra the carrier of X):]
[: the carrier of (CAlgebra the carrier of X), the carrier of (CAlgebra the carrier of X):] is non empty set
[:[: the carrier of (CAlgebra the carrier of X), the carrier of (CAlgebra the carrier of X):], the carrier of (CAlgebra the carrier of X):] is non empty set
bool [:[: the carrier of (CAlgebra the carrier of X), the carrier of (CAlgebra the carrier of X):], the carrier of (CAlgebra the carrier of X):] is non empty set
the addF of (CAlgebra the carrier of X) . (G,FB) is Element of the carrier of (CAlgebra the carrier of X)
[G,FB] is set
{G,FB} is non empty set
{G} is non empty set
{{G,FB},{G}} is non empty set
the addF of (CAlgebra the carrier of X) . [G,FB] is set
GB is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
aFB is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
aF is Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs ( the carrier of X,COMPLEX)
dom GB is Element of bool the carrier of X
bool the carrier of X is non empty set
dom aFB is Element of bool the carrier of X
(dom GB) /\ (dom aFB) is Element of bool the carrier of X
the carrier of X /\ (dom aFB) is Element of bool the carrier of X
the carrier of X /\ the carrier of X is set
dom aF is Element of bool the carrier of X
aG is set
aF . aG is complex set
GB . aG is complex set
aFB . aG is complex set
(GB . aG) + (aFB . aG) is complex set
GB + aFB is Relation-like the carrier of X -defined Function-like total V139() set
aG is Relation-like Function-like set
dom aG is set
rng aG is set
G is Element of the carrier of (CAlgebra the carrier of X)
- G is Element of the carrier of (CAlgebra the carrier of X)
FB is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
GB is Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs ( the carrier of X,COMPLEX)
aF is complex set
aF * G is Element of the carrier of (CAlgebra the carrier of X)
the Mult of (CAlgebra the carrier of X) is non empty Relation-like [:COMPLEX, the carrier of (CAlgebra the carrier of X):] -defined the carrier of (CAlgebra the carrier of X) -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of (CAlgebra the carrier of X):], the carrier of (CAlgebra the carrier of X):]
[:COMPLEX, the carrier of (CAlgebra the carrier of X):] is non empty set
[:[:COMPLEX, the carrier of (CAlgebra the carrier of X):], the carrier of (CAlgebra the carrier of X):] is non empty set
bool [:[:COMPLEX, the carrier of (CAlgebra the carrier of X):], the carrier of (CAlgebra the carrier of X):] is non empty set
[aF,G] is set
{aF,G} is non empty set
{aF} is non empty V176() set
{{aF,G},{aF}} is non empty set
the Mult of (CAlgebra the carrier of X) . [aF,G] is set
dom FB is Element of bool the carrier of X
bool the carrier of X is non empty set
aG is set
dom GB is Element of bool the carrier of X
GB . aG is complex set
- 1 is non empty complex real ext-real non positive negative Element of REAL
aFB is Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs ( the carrier of X,COMPLEX)
r is Element of the carrier of X
aFB . r is complex Element of COMPLEX
(- 1) * (aFB . r) is complex set
FB . aG is complex set
- (FB . aG) is complex set
- FB is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
- 1 is non empty complex real ext-real non positive negative set
(- 1) (#) FB is Relation-like the carrier of X -defined Function-like total V139() set
aG is Relation-like Function-like set
dom aG is set
rng aG is set
aF (#) FB is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
G is complex set
FB is Element of the carrier of (CAlgebra the carrier of X)
G * FB is Element of the carrier of (CAlgebra the carrier of X)
the Mult of (CAlgebra the carrier of X) is non empty Relation-like [:COMPLEX, the carrier of (CAlgebra the carrier of X):] -defined the carrier of (CAlgebra the carrier of X) -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of (CAlgebra the carrier of X):], the carrier of (CAlgebra the carrier of X):]
[:COMPLEX, the carrier of (CAlgebra the carrier of X):] is non empty set
[:[:COMPLEX, the carrier of (CAlgebra the carrier of X):], the carrier of (CAlgebra the carrier of X):] is non empty set
bool [:[:COMPLEX, the carrier of (CAlgebra the carrier of X):], the carrier of (CAlgebra the carrier of X):] is non empty set
[G,FB] is set
{G,FB} is non empty set
{G} is non empty V176() set
{{G,FB},{G}} is non empty set
the Mult of (CAlgebra the carrier of X) . [G,FB] is set
GB is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
aFB is Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs ( the carrier of X,COMPLEX)
dom GB is Element of bool the carrier of X
bool the carrier of X is non empty set
dom aFB is Element of bool the carrier of X
aF is set
aFB . aF is complex set
GB . aF is complex set
G * (GB . aF) is complex set
G (#) GB is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
aF is Relation-like Function-like set
dom aF is set
rng aF is set
G is Element of the carrier of (CAlgebra the carrier of X)
FB is Element of the carrier of (CAlgebra the carrier of X)
G * FB is Element of the carrier of (CAlgebra the carrier of X)
the multF of (CAlgebra the carrier of X) is non empty Relation-like [: the carrier of (CAlgebra the carrier of X), the carrier of (CAlgebra the carrier of X):] -defined the carrier of (CAlgebra the carrier of X) -valued Function-like total quasi_total Element of bool [:[: the carrier of (CAlgebra the carrier of X), the carrier of (CAlgebra the carrier of X):], the carrier of (CAlgebra the carrier of X):]
[: the carrier of (CAlgebra the carrier of X), the carrier of (CAlgebra the carrier of X):] is non empty set
[:[: the carrier of (CAlgebra the carrier of X), the carrier of (CAlgebra the carrier of X):], the carrier of (CAlgebra the carrier of X):] is non empty set
bool [:[: the carrier of (CAlgebra the carrier of X), the carrier of (CAlgebra the carrier of X):], the carrier of (CAlgebra the carrier of X):] is non empty set
the multF of (CAlgebra the carrier of X) . (G,FB) is Element of the carrier of (CAlgebra the carrier of X)
[G,FB] is set
{G,FB} is non empty set
{G} is non empty set
{{G,FB},{G}} is non empty set
the multF of (CAlgebra the carrier of X) . [G,FB] is set
GB is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
aFB is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
aF is Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs ( the carrier of X,COMPLEX)
dom GB is Element of bool the carrier of X
bool the carrier of X is non empty set
dom aFB is Element of bool the carrier of X
(dom GB) /\ (dom aFB) is Element of bool the carrier of X
the carrier of X /\ (dom aFB) is Element of bool the carrier of X
the carrier of X /\ the carrier of X is set
dom aF is Element of bool the carrier of X
aG is set
aF . aG is complex set
GB . aG is complex set
aFB . aG is complex set
(GB . aG) * (aFB . aG) is complex set
GB (#) aFB is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
aG is Relation-like Function-like set
dom aG is set
rng aG is set
G is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
(X,1r) is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:]
the carrier of X --> 1r is non empty Relation-like the carrier of X -defined {1r} -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,{1r}:]
{1r} is non empty V176() set
[: the carrier of X,{1r}:] is non empty V139() set
bool [: the carrier of X,{1r}:] is non empty set
1. (CAlgebra the carrier of X) is Element of the carrier of (CAlgebra the carrier of X)
the OneF of (CAlgebra the carrier of X) is Element of the carrier of (CAlgebra the carrier of X)
X is non empty TopSpace-like TopStruct
(X) is non empty multiplicatively-closed Cadditively-linearly-closed Element of bool the carrier of (CAlgebra the carrier of X)
the carrier of X is non empty set
CAlgebra the carrier of X is non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital strict vector-associative ComplexAlgebraStr
Funcs ( the carrier of X,COMPLEX) is non empty functional FUNCTION_DOMAIN of the carrier of X, COMPLEX
ComplexFuncMult the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):] -defined Funcs ( the carrier of X,COMPLEX) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):]
[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):] is non empty set
[:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
bool [:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
ComplexFuncAdd the carrier of X is non empty Relation-like [:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):] -defined Funcs ( the carrier of X,COMPLEX) -valued Function-like total quasi_total Element of bool [:[:(Funcs ( the carrier of X,COMPLEX)),(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):]
ComplexFuncExtMult the carrier of X is non empty Relation-like [:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):] -defined Funcs ( the carrier of X,COMPLEX) -valued Function-like total quasi_total Element of bool [:[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):]
[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):] is non empty set
[:[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
bool [:[:COMPLEX,(Funcs ( the carrier of X,COMPLEX)):],(Funcs ( the carrier of X,COMPLEX)):] is non empty set
ComplexFuncUnit the carrier of X is Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs ( the carrier of X,COMPLEX)
the carrier of X --> 1r is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [: the carrier of X,COMPLEX:]
[: the carrier of X,COMPLEX:] is non empty V139() set
bool [: the carrier of X,COMPLEX:] is non empty set
ComplexFuncZero the carrier of X is Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs ( the carrier of X,COMPLEX)
the carrier of X --> 0 is non empty Relation-like the carrier of X -defined REAL -valued RAT -valued INT -valued Function-like total quasi_total V139() V140() V141() V142() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty V139() V140() V141() set
bool [: the carrier of X,REAL:] is non empty set
ComplexAlgebraStr(# (Funcs ( the carrier of X,COMPLEX)),(ComplexFuncMult the carrier of X),(ComplexFuncAdd the carrier of X),(ComplexFuncExtMult the carrier of X),(ComplexFuncUnit the carrier of X),(ComplexFuncZero the carrier of X) #) is strict ComplexAlgebraStr
the carrier of (CAlgebra the carrier of X) is non empty set
bool the carrier of (CAlgebra the carrier of X) is non empty set
{ b1 where b1 is non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() (X) Element of bool [: the carrier of X,COMPLEX:] : verum } is set
mult_ ((X),(CAlgebra the carrier of X)) is non empty Relation-like [:(X),(X):] -defined (X) -valued Function-like total quasi_total Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is non empty set
[:[:(X),(X):],(X):] is non empty set
bool [:[:(X),(X):],(X):] is non empty set
Add_ ((X),(CAlgebra the carrier of X)) is non empty Relation-like [:(X),(X):] -defined (X) -valued Function-like total quasi_total Element of bool [: