:: CC0SP2 semantic presentation

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

{ b

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 " { b

r is V176() Element of bool COMPLEX

r is Element of bool the carrier of X

X .: (X " { b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

c

c

c

|.(c

(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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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