:: CONVEX4 semantic presentation

REAL is non empty non trivial non finite V68() V69() V70() V74() set

NAT is non trivial ordinal non finite cardinal limit_cardinal V68() V69() V70() V71() V72() V73() V74() Element of bool REAL

bool REAL is non empty non trivial non finite set

omega is non trivial ordinal non finite cardinal limit_cardinal V68() V69() V70() V71() V72() V73() V74() set

bool omega is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

COMPLEX is non empty non trivial non finite V68() V74() set

RAT is non empty non trivial non finite V68() V69() V70() V71() V74() set

INT is non empty non trivial non finite V68() V69() V70() V71() V72() V74() set

[:COMPLEX,COMPLEX:] is non empty non trivial non finite V58() set

bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite V58() set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set

[:REAL,REAL:] is non empty non trivial non finite V58() V59() V60() set

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

[:[:REAL,REAL:],REAL:] is non empty non trivial non finite V58() V59() V60() set

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

[:RAT,RAT:] is non empty non trivial RAT -valued non finite V58() V59() V60() set

bool [:RAT,RAT:] is non empty non trivial non finite set

[:[:RAT,RAT:],RAT:] is non empty non trivial RAT -valued non finite V58() V59() V60() set

bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set

[:INT,INT:] is non empty non trivial RAT -valued INT -valued non finite V58() V59() V60() set

bool [:INT,INT:] is non empty non trivial non finite set

[:[:INT,INT:],INT:] is non empty non trivial RAT -valued INT -valued non finite V58() V59() V60() set

bool [:[:INT,INT:],INT:] is non empty non trivial non finite set

[:NAT,NAT:] is RAT -valued INT -valued V58() V59() V60() V61() set

[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued V58() V59() V60() V61() set

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

K294(NAT) is V54() set

{} is empty ordinal natural complex real finite V42() cardinal {} -element ext-real non positive non negative V68() V69() V70() V71() V72() V73() V74() set

the empty ordinal natural complex real finite V42() cardinal {} -element ext-real non positive non negative V68() V69() V70() V71() V72() V73() V74() set is empty ordinal natural complex real finite V42() cardinal {} -element ext-real non positive non negative V68() V69() V70() V71() V72() V73() V74() set

2 is non empty ordinal natural complex real finite cardinal V49() V50() ext-real positive non negative V68() V69() V70() V71() V72() V73() Element of NAT

[:NAT,REAL:] is non trivial non finite V58() V59() V60() set

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

[:NAT,COMPLEX:] is non trivial non finite V58() set

bool [:NAT,COMPLEX:] is non empty non trivial non finite set

the_set_of_ComplexSequences is non empty set

[:the_set_of_ComplexSequences,the_set_of_ComplexSequences:] is non empty set

[:[:the_set_of_ComplexSequences,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:] is non empty set

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

[:COMPLEX,the_set_of_ComplexSequences:] is non empty non trivial non finite set

[:[:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:] is non empty non trivial non finite set

bool [:[:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:] is non empty non trivial non finite set

Linear_Space_of_ComplexSequences is non empty left_complementable right_complementable Abelian add-associative right_zeroed V138() strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct

the carrier of Linear_Space_of_ComplexSequences is non empty set

bool the carrier of Linear_Space_of_ComplexSequences is non empty set

the_set_of_l2ComplexSequences is Element of bool the carrier of Linear_Space_of_ComplexSequences

[:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:] is set

[:[:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX:] is V58() set

bool [:[:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX:] is non empty set

1 is non empty ordinal natural complex real finite cardinal V49() V50() ext-real positive non negative V68() V69() V70() V71() V72() V73() Element of NAT

<*> REAL is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V58() V59() V60() FinSequence of REAL

Sum (<*> REAL) is complex real ext-real Element of REAL

K267() is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V58() V59() V60() Element of bool [:[:REAL,REAL:],REAL:]

K295(REAL,(<*> REAL),K267()) is complex real ext-real Element of REAL

0 is empty ordinal natural complex real finite V42() cardinal {} -element V49() V50() ext-real non positive non negative V68() V69() V70() V71() V72() V73() V74() Element of NAT

len {} is empty ordinal natural complex real finite V42() cardinal {} -element ext-real non positive non negative V68() V69() V70() V71() V72() V73() V74() set

3 is non empty ordinal natural complex real finite cardinal V49() V50() ext-real positive non negative V68() V69() V70() V71() V72() V73() Element of NAT

Seg 1 is V68() V69() V70() V71() V72() V73() Element of bool NAT

{ b

{1} is non empty trivial finite V42() 1 -element V68() V69() V70() V71() V72() V73() set

Seg 2 is V68() V69() V70() V71() V72() V73() Element of bool NAT

{ b

{1,2} is non empty finite V42() V68() V69() V70() V71() V72() V73() set

Seg 3 is V68() V69() V70() V71() V72() V73() Element of bool NAT

{ b

K198(1,2,3) is non empty finite V68() V69() V70() V71() V72() V73() set

[:2,REAL:] is non empty non trivial non finite V58() V59() V60() set

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

1r is complex Element of COMPLEX

- 1r is complex Element of COMPLEX

V is non empty 1-sorted

the carrier of V is non empty set

Funcs ( the carrier of V,COMPLEX) is non empty functional FUNCTION_DOMAIN of the carrier of V, COMPLEX

bool the carrier of V is non empty set

0c is empty ordinal natural complex real finite V42() cardinal {} -element ext-real non positive non negative V68() V69() V70() V71() V72() V73() V74() Element of COMPLEX

the carrier of V --> 0c is non empty Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() V59() V60() V61() Element of bool [: the carrier of V,COMPLEX:]

[: the carrier of V,COMPLEX:] is non empty non trivial non finite V58() set

bool [: the carrier of V,COMPLEX:] is non empty non trivial non finite set

M is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() Element of Funcs ( the carrier of V,COMPLEX)

{} V is empty proper ordinal natural complex real finite V42() cardinal {} -element ext-real non positive non negative V68() V69() V70() V71() V72() V73() V74() Element of bool the carrier of V

N is Element of the carrier of V

M . N is complex Element of COMPLEX

V is non empty addLoopStr

the carrier of V is non empty set

Funcs ( the carrier of V,COMPLEX) is non empty functional FUNCTION_DOMAIN of the carrier of V, COMPLEX

V is non empty addLoopStr

the carrier of V is non empty set

Funcs ( the carrier of V,COMPLEX) is non empty functional FUNCTION_DOMAIN of the carrier of V, COMPLEX

M is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() Element of Funcs ( the carrier of V,COMPLEX)

support M is set

dom M is Element of bool the carrier of V

bool the carrier of V is non empty set

N is set

V is non empty addLoopStr

the carrier of V is non empty set

Funcs ( the carrier of V,COMPLEX) is non empty functional FUNCTION_DOMAIN of the carrier of V, COMPLEX

M is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() Element of Funcs ( the carrier of V,COMPLEX)

support M is set

bool the carrier of V is non empty set

0c is empty ordinal natural complex real finite V42() cardinal {} -element ext-real non positive non negative V68() V69() V70() V71() V72() V73() V74() Element of COMPLEX

{ b

N is Element of bool the carrier of V

{ b

r2 is set

M . r2 is complex set

r2 is set

r1 is Element of the carrier of V

M . r1 is complex Element of COMPLEX

r2 is set

r1 is Element of the carrier of V

M . r1 is complex Element of COMPLEX

r2 is set

M . r2 is complex set

V is non empty addLoopStr

the carrier of V is non empty set

M is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V)

(V,M) is Element of bool the carrier of V

bool the carrier of V is non empty set

{ b

SG is finite Element of bool the carrier of V

Y is set

r2 is Element of the carrier of V

M . r2 is complex Element of COMPLEX

V is non empty addLoopStr

the carrier of V is non empty set

M is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V)

(V,M) is finite Element of bool the carrier of V

bool the carrier of V is non empty set

{ b

N is Element of the carrier of V

M . N is complex Element of COMPLEX

SG is Element of the carrier of V

M . SG is complex Element of COMPLEX

V is non empty addLoopStr

the carrier of V is non empty set

Funcs ( the carrier of V,COMPLEX) is non empty functional FUNCTION_DOMAIN of the carrier of V, COMPLEX

the carrier of V --> 0c is non empty Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() V59() V60() V61() Element of bool [: the carrier of V,COMPLEX:]

[: the carrier of V,COMPLEX:] is non empty non trivial non finite V58() set

bool [: the carrier of V,COMPLEX:] is non empty non trivial non finite set

M is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() Element of Funcs ( the carrier of V,COMPLEX)

{} V is empty proper ordinal natural complex real finite V42() cardinal {} -element ext-real non positive non negative V68() V69() V70() V71() V72() V73() V74() Element of bool the carrier of V

bool the carrier of V is non empty set

N is Element of the carrier of V

M . N is complex Element of COMPLEX

N is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V)

(V,N) is finite Element of bool the carrier of V

bool the carrier of V is non empty set

{ b

the Element of { b

r2 is Element of the carrier of V

N . r2 is complex Element of COMPLEX

M is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V)

(V,M) is finite Element of bool the carrier of V

bool the carrier of V is non empty set

{ b

N is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V)

(V,N) is finite Element of bool the carrier of V

{ b

SG is set

Y is Element of the carrier of V

N . Y is complex Element of COMPLEX

M . Y is complex Element of COMPLEX

M . SG is complex set

N . SG is complex set

V is non empty addLoopStr

(V) is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V)

the carrier of V is non empty set

(V,(V)) is finite Element of bool the carrier of V

bool the carrier of V is non empty set

{ b

V is non empty addLoopStr

the carrier of V is non empty set

(V) is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V)

M is Element of the carrier of V

(V) . M is complex Element of COMPLEX

(V,(V)) is empty proper ordinal natural complex real finite V42() cardinal {} -element ext-real non positive non negative V68() V69() V70() V71() V72() V73() V74() Element of bool the carrier of V

bool the carrier of V is non empty set

{ b

V is non empty addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

M is Element of bool the carrier of V

(V) is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V)

N is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V)

(V,N) is finite Element of bool the carrier of V

{ b

V is non empty addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

M is Element of bool the carrier of V

N is Element of bool the carrier of V

SG is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V,M)

(V,SG) is finite Element of bool the carrier of V

{ b

V is non empty addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

(V) is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V)

M is Element of bool the carrier of V

(V,(V)) is empty proper ordinal natural complex real finite V42() cardinal {} -element ext-real non positive non negative V68() V69() V70() V71() V72() V73() V74() Element of bool the carrier of V

{ b

V is non empty addLoopStr

the carrier of V is non empty set

{} the carrier of V is empty proper ordinal natural complex real finite V42() cardinal {} -element ext-real non positive non negative V68() V69() V70() V71() V72() V73() V74() Element of bool the carrier of V

bool the carrier of V is non empty set

(V) is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V)

M is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V, {} the carrier of V)

(V,M) is finite Element of bool the carrier of V

{ b

V is non empty CLSStruct

the carrier of V is non empty set

[: the carrier of V,COMPLEX:] is non empty non trivial non finite V58() set

bool [: the carrier of V,COMPLEX:] is non empty non trivial non finite set

M is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

len M is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

N is non empty Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() Element of bool [: the carrier of V,COMPLEX:]

SG is Relation-like Function-like FinSequence-like set

len SG is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

dom SG is V68() V69() V70() V71() V72() V73() Element of bool NAT

rng SG is set

Y is set

r2 is set

SG . r2 is set

r1 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

SG . r1 is set

M /. r1 is Element of the carrier of V

N . (M /. r1) is complex Element of COMPLEX

(N . (M /. r1)) * (M /. r1) is Element of the carrier of V

the Mult of V is non empty Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]

[:COMPLEX, the carrier of V:] is non empty non trivial non finite set

[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

[(N . (M /. r1)),(M /. r1)] is set

{(N . (M /. r1)),(M /. r1)} is non empty finite set

{(N . (M /. r1))} is non empty trivial finite 1 -element V68() set

{{(N . (M /. r1)),(M /. r1)},{(N . (M /. r1))}} is non empty finite V42() set

the Mult of V . [(N . (M /. r1)),(M /. r1)] is set

Y is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

len Y is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

dom Y is V68() V69() V70() V71() V72() V73() Element of bool NAT

r2 is ordinal natural complex real finite cardinal ext-real non negative set

Y . r2 is set

M /. r2 is Element of the carrier of V

N . (M /. r2) is complex Element of COMPLEX

(N . (M /. r2)) * (M /. r2) is Element of the carrier of V

the Mult of V is non empty Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]

[:COMPLEX, the carrier of V:] is non empty non trivial non finite set

[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

[(N . (M /. r2)),(M /. r2)] is set

{(N . (M /. r2)),(M /. r2)} is non empty finite set

{(N . (M /. r2))} is non empty trivial finite 1 -element V68() set

{{(N . (M /. r2)),(M /. r2)},{(N . (M /. r2))}} is non empty finite V42() set

the Mult of V . [(N . (M /. r2)),(M /. r2)] is set

SG is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

len SG is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

dom SG is V68() V69() V70() V71() V72() V73() Element of bool NAT

Y is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

len Y is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

dom Y is V68() V69() V70() V71() V72() V73() Element of bool NAT

r2 is ordinal natural complex real finite cardinal ext-real non negative set

Seg (len SG) is V68() V69() V70() V71() V72() V73() Element of bool NAT

{ b

SG . r2 is set

M /. r2 is Element of the carrier of V

N . (M /. r2) is complex Element of COMPLEX

(N . (M /. r2)) * (M /. r2) is Element of the carrier of V

the Mult of V is non empty Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]

[:COMPLEX, the carrier of V:] is non empty non trivial non finite set

[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

[(N . (M /. r2)),(M /. r2)] is set

{(N . (M /. r2)),(M /. r2)} is non empty finite set

{(N . (M /. r2))} is non empty trivial finite 1 -element V68() set

{{(N . (M /. r2)),(M /. r2)},{(N . (M /. r2))}} is non empty finite V42() set

the Mult of V . [(N . (M /. r2)),(M /. r2)] is set

Y . r2 is set

V is non empty CLSStruct

the carrier of V is non empty set

[: the carrier of V,COMPLEX:] is non empty non trivial non finite V58() set

bool [: the carrier of V,COMPLEX:] is non empty non trivial non finite set

M is Element of the carrier of V

N is set

SG is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

dom SG is V68() V69() V70() V71() V72() V73() Element of bool NAT

SG . N is set

Y is non empty Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() Element of bool [: the carrier of V,COMPLEX:]

(V,SG,Y) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

(V,SG,Y) . N is set

Y . M is complex Element of COMPLEX

(Y . M) * M is Element of the carrier of V

the Mult of V is non empty Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]

[:COMPLEX, the carrier of V:] is non empty non trivial non finite set

[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

[(Y . M),M] is set

{(Y . M),M} is non empty finite set

{(Y . M)} is non empty trivial finite 1 -element V68() set

{{(Y . M),M},{(Y . M)}} is non empty finite V42() set

the Mult of V . [(Y . M),M] is set

SG /. N is Element of the carrier of V

len (V,SG,Y) is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

len SG is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

dom (V,SG,Y) is V68() V69() V70() V71() V72() V73() Element of bool NAT

V is non empty CLSStruct

the carrier of V is non empty set

[: the carrier of V,COMPLEX:] is non empty non trivial non finite V58() set

bool [: the carrier of V,COMPLEX:] is non empty non trivial non finite set

<*> the carrier of V is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

M is non empty Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() Element of bool [: the carrier of V,COMPLEX:]

(V,(<*> the carrier of V),M) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

len (V,(<*> the carrier of V),M) is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

len (<*> the carrier of V) is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

V is non empty CLSStruct

the carrier of V is non empty set

[: the carrier of V,COMPLEX:] is non empty non trivial non finite V58() set

bool [: the carrier of V,COMPLEX:] is non empty non trivial non finite set

M is Element of the carrier of V

<*M*> is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

[1,M] is set

{1,M} is non empty finite set

{{1,M},{1}} is non empty finite V42() set

{[1,M]} is non empty trivial finite 1 -element set

N is non empty Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() Element of bool [: the carrier of V,COMPLEX:]

(V,<*M*>,N) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

N . M is complex Element of COMPLEX

(N . M) * M is Element of the carrier of V

the Mult of V is non empty Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]

[:COMPLEX, the carrier of V:] is non empty non trivial non finite set

[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

[(N . M),M] is set

{(N . M),M} is non empty finite set

{(N . M)} is non empty trivial finite 1 -element V68() set

{{(N . M),M},{(N . M)}} is non empty finite V42() set

the Mult of V . [(N . M),M] is set

<*((N . M) * M)*> is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

[1,((N . M) * M)] is set

{1,((N . M) * M)} is non empty finite set

{{1,((N . M) * M)},{1}} is non empty finite V42() set

{[1,((N . M) * M)]} is non empty trivial finite 1 -element set

{1} is non empty trivial finite V42() 1 -element V68() V69() V70() V71() V72() V73() Element of bool REAL

len (V,<*M*>,N) is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

len <*M*> is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

dom (V,<*M*>,N) is V68() V69() V70() V71() V72() V73() Element of bool NAT

(V,<*M*>,N) . 1 is set

<*M*> /. 1 is Element of the carrier of V

N . (<*M*> /. 1) is complex Element of COMPLEX

(N . (<*M*> /. 1)) * (<*M*> /. 1) is Element of the carrier of V

[(N . (<*M*> /. 1)),(<*M*> /. 1)] is set

{(N . (<*M*> /. 1)),(<*M*> /. 1)} is non empty finite set

{(N . (<*M*> /. 1))} is non empty trivial finite 1 -element V68() set

{{(N . (<*M*> /. 1)),(<*M*> /. 1)},{(N . (<*M*> /. 1))}} is non empty finite V42() set

the Mult of V . [(N . (<*M*> /. 1)),(<*M*> /. 1)] is set

(N . (<*M*> /. 1)) * M is Element of the carrier of V

[(N . (<*M*> /. 1)),M] is set

{(N . (<*M*> /. 1)),M} is non empty finite set

{{(N . (<*M*> /. 1)),M},{(N . (<*M*> /. 1))}} is non empty finite V42() set

the Mult of V . [(N . (<*M*> /. 1)),M] is set

V is non empty CLSStruct

the carrier of V is non empty set

[: the carrier of V,COMPLEX:] is non empty non trivial non finite V58() set

bool [: the carrier of V,COMPLEX:] is non empty non trivial non finite set

M is Element of the carrier of V

N is Element of the carrier of V

<*M,N*> is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

<*M*> is Relation-like Function-like set

[1,M] is set

{1,M} is non empty finite set

{{1,M},{1}} is non empty finite V42() set

{[1,M]} is non empty trivial finite 1 -element set

<*N*> is Relation-like Function-like set

[1,N] is set

{1,N} is non empty finite set

{{1,N},{1}} is non empty finite V42() set

{[1,N]} is non empty trivial finite 1 -element set

K158(<*M*>,<*N*>) is Relation-like Function-like FinSequence-like set

SG is non empty Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() Element of bool [: the carrier of V,COMPLEX:]

(V,<*M,N*>,SG) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

SG . M is complex Element of COMPLEX

(SG . M) * M is Element of the carrier of V

the Mult of V is non empty Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]

[:COMPLEX, the carrier of V:] is non empty non trivial non finite set

[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

[(SG . M),M] is set

{(SG . M),M} is non empty finite set

{(SG . M)} is non empty trivial finite 1 -element V68() set

{{(SG . M),M},{(SG . M)}} is non empty finite V42() set

the Mult of V . [(SG . M),M] is set

SG . N is complex Element of COMPLEX

(SG . N) * N is Element of the carrier of V

[(SG . N),N] is set

{(SG . N),N} is non empty finite set

{(SG . N)} is non empty trivial finite 1 -element V68() set

{{(SG . N),N},{(SG . N)}} is non empty finite V42() set

the Mult of V . [(SG . N),N] is set

<*((SG . M) * M),((SG . N) * N)*> is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

<*((SG . M) * M)*> is Relation-like Function-like set

[1,((SG . M) * M)] is set

{1,((SG . M) * M)} is non empty finite set

{{1,((SG . M) * M)},{1}} is non empty finite V42() set

{[1,((SG . M) * M)]} is non empty trivial finite 1 -element set

<*((SG . N) * N)*> is Relation-like Function-like set

[1,((SG . N) * N)] is set

{1,((SG . N) * N)} is non empty finite set

{{1,((SG . N) * N)},{1}} is non empty finite V42() set

{[1,((SG . N) * N)]} is non empty trivial finite 1 -element set

K158(<*((SG . M) * M)*>,<*((SG . N) * N)*>) is Relation-like Function-like FinSequence-like set

len (V,<*M,N*>,SG) is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

len <*M,N*> is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

dom (V,<*M,N*>,SG) is V68() V69() V70() V71() V72() V73() Element of bool NAT

{1,2} is non empty finite V42() V68() V69() V70() V71() V72() V73() Element of bool REAL

(V,<*M,N*>,SG) . 2 is set

<*M,N*> /. 2 is Element of the carrier of V

SG . (<*M,N*> /. 2) is complex Element of COMPLEX

(SG . (<*M,N*> /. 2)) * (<*M,N*> /. 2) is Element of the carrier of V

[(SG . (<*M,N*> /. 2)),(<*M,N*> /. 2)] is set

{(SG . (<*M,N*> /. 2)),(<*M,N*> /. 2)} is non empty finite set

{(SG . (<*M,N*> /. 2))} is non empty trivial finite 1 -element V68() set

{{(SG . (<*M,N*> /. 2)),(<*M,N*> /. 2)},{(SG . (<*M,N*> /. 2))}} is non empty finite V42() set

the Mult of V . [(SG . (<*M,N*> /. 2)),(<*M,N*> /. 2)] is set

(SG . (<*M,N*> /. 2)) * N is Element of the carrier of V

[(SG . (<*M,N*> /. 2)),N] is set

{(SG . (<*M,N*> /. 2)),N} is non empty finite set

{{(SG . (<*M,N*> /. 2)),N},{(SG . (<*M,N*> /. 2))}} is non empty finite V42() set

the Mult of V . [(SG . (<*M,N*> /. 2)),N] is set

(V,<*M,N*>,SG) . 1 is set

<*M,N*> /. 1 is Element of the carrier of V

SG . (<*M,N*> /. 1) is complex Element of COMPLEX

(SG . (<*M,N*> /. 1)) * (<*M,N*> /. 1) is Element of the carrier of V

[(SG . (<*M,N*> /. 1)),(<*M,N*> /. 1)] is set

{(SG . (<*M,N*> /. 1)),(<*M,N*> /. 1)} is non empty finite set

{(SG . (<*M,N*> /. 1))} is non empty trivial finite 1 -element V68() set

{{(SG . (<*M,N*> /. 1)),(<*M,N*> /. 1)},{(SG . (<*M,N*> /. 1))}} is non empty finite V42() set

the Mult of V . [(SG . (<*M,N*> /. 1)),(<*M,N*> /. 1)] is set

(SG . (<*M,N*> /. 1)) * M is Element of the carrier of V

[(SG . (<*M,N*> /. 1)),M] is set

{(SG . (<*M,N*> /. 1)),M} is non empty finite set

{{(SG . (<*M,N*> /. 1)),M},{(SG . (<*M,N*> /. 1))}} is non empty finite V42() set

the Mult of V . [(SG . (<*M,N*> /. 1)),M] is set

V is non empty CLSStruct

the carrier of V is non empty set

[: the carrier of V,COMPLEX:] is non empty non trivial non finite V58() set

bool [: the carrier of V,COMPLEX:] is non empty non trivial non finite set

M is Element of the carrier of V

N is Element of the carrier of V

SG is Element of the carrier of V

<*M,N,SG*> is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

<*M*> is Relation-like Function-like set

[1,M] is set

{1,M} is non empty finite set

{{1,M},{1}} is non empty finite V42() set

{[1,M]} is non empty trivial finite 1 -element set

<*N*> is Relation-like Function-like set

[1,N] is set

{1,N} is non empty finite set

{{1,N},{1}} is non empty finite V42() set

{[1,N]} is non empty trivial finite 1 -element set

K158(<*M*>,<*N*>) is Relation-like Function-like FinSequence-like set

<*SG*> is Relation-like Function-like set

[1,SG] is set

{1,SG} is non empty finite set

{{1,SG},{1}} is non empty finite V42() set

{[1,SG]} is non empty trivial finite 1 -element set

K158(K158(<*M*>,<*N*>),<*SG*>) is Relation-like Function-like FinSequence-like set

Y is non empty Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() Element of bool [: the carrier of V,COMPLEX:]

(V,<*M,N,SG*>,Y) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

Y . M is complex Element of COMPLEX

(Y . M) * M is Element of the carrier of V

the Mult of V is non empty Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]

[:COMPLEX, the carrier of V:] is non empty non trivial non finite set

[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

[(Y . M),M] is set

{(Y . M),M} is non empty finite set

{(Y . M)} is non empty trivial finite 1 -element V68() set

{{(Y . M),M},{(Y . M)}} is non empty finite V42() set

the Mult of V . [(Y . M),M] is set

Y . N is complex Element of COMPLEX

(Y . N) * N is Element of the carrier of V

[(Y . N),N] is set

{(Y . N),N} is non empty finite set

{(Y . N)} is non empty trivial finite 1 -element V68() set

{{(Y . N),N},{(Y . N)}} is non empty finite V42() set

the Mult of V . [(Y . N),N] is set

Y . SG is complex Element of COMPLEX

(Y . SG) * SG is Element of the carrier of V

[(Y . SG),SG] is set

{(Y . SG),SG} is non empty finite set

{(Y . SG)} is non empty trivial finite 1 -element V68() set

{{(Y . SG),SG},{(Y . SG)}} is non empty finite V42() set

the Mult of V . [(Y . SG),SG] is set

<*((Y . M) * M),((Y . N) * N),((Y . SG) * SG)*> is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

<*((Y . M) * M)*> is Relation-like Function-like set

[1,((Y . M) * M)] is set

{1,((Y . M) * M)} is non empty finite set

{{1,((Y . M) * M)},{1}} is non empty finite V42() set

{[1,((Y . M) * M)]} is non empty trivial finite 1 -element set

<*((Y . N) * N)*> is Relation-like Function-like set

[1,((Y . N) * N)] is set

{1,((Y . N) * N)} is non empty finite set

{{1,((Y . N) * N)},{1}} is non empty finite V42() set

{[1,((Y . N) * N)]} is non empty trivial finite 1 -element set

K158(<*((Y . M) * M)*>,<*((Y . N) * N)*>) is Relation-like Function-like FinSequence-like set

<*((Y . SG) * SG)*> is Relation-like Function-like set

[1,((Y . SG) * SG)] is set

{1,((Y . SG) * SG)} is non empty finite set

{{1,((Y . SG) * SG)},{1}} is non empty finite V42() set

{[1,((Y . SG) * SG)]} is non empty trivial finite 1 -element set

K158(K158(<*((Y . M) * M)*>,<*((Y . N) * N)*>),<*((Y . SG) * SG)*>) is Relation-like Function-like FinSequence-like set

len (V,<*M,N,SG*>,Y) is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

len <*M,N,SG*> is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

dom (V,<*M,N,SG*>,Y) is V68() V69() V70() V71() V72() V73() Element of bool NAT

{1,2,3} is non empty finite V68() V69() V70() V71() V72() V73() Element of bool REAL

(V,<*M,N,SG*>,Y) . 3 is set

<*M,N,SG*> /. 3 is Element of the carrier of V

Y . (<*M,N,SG*> /. 3) is complex Element of COMPLEX

(Y . (<*M,N,SG*> /. 3)) * (<*M,N,SG*> /. 3) is Element of the carrier of V

[(Y . (<*M,N,SG*> /. 3)),(<*M,N,SG*> /. 3)] is set

{(Y . (<*M,N,SG*> /. 3)),(<*M,N,SG*> /. 3)} is non empty finite set

{(Y . (<*M,N,SG*> /. 3))} is non empty trivial finite 1 -element V68() set

{{(Y . (<*M,N,SG*> /. 3)),(<*M,N,SG*> /. 3)},{(Y . (<*M,N,SG*> /. 3))}} is non empty finite V42() set

the Mult of V . [(Y . (<*M,N,SG*> /. 3)),(<*M,N,SG*> /. 3)] is set

(Y . (<*M,N,SG*> /. 3)) * SG is Element of the carrier of V

[(Y . (<*M,N,SG*> /. 3)),SG] is set

{(Y . (<*M,N,SG*> /. 3)),SG} is non empty finite set

{{(Y . (<*M,N,SG*> /. 3)),SG},{(Y . (<*M,N,SG*> /. 3))}} is non empty finite V42() set

the Mult of V . [(Y . (<*M,N,SG*> /. 3)),SG] is set

(V,<*M,N,SG*>,Y) . 2 is set

<*M,N,SG*> /. 2 is Element of the carrier of V

Y . (<*M,N,SG*> /. 2) is complex Element of COMPLEX

(Y . (<*M,N,SG*> /. 2)) * (<*M,N,SG*> /. 2) is Element of the carrier of V

[(Y . (<*M,N,SG*> /. 2)),(<*M,N,SG*> /. 2)] is set

{(Y . (<*M,N,SG*> /. 2)),(<*M,N,SG*> /. 2)} is non empty finite set

{(Y . (<*M,N,SG*> /. 2))} is non empty trivial finite 1 -element V68() set

{{(Y . (<*M,N,SG*> /. 2)),(<*M,N,SG*> /. 2)},{(Y . (<*M,N,SG*> /. 2))}} is non empty finite V42() set

the Mult of V . [(Y . (<*M,N,SG*> /. 2)),(<*M,N,SG*> /. 2)] is set

(Y . (<*M,N,SG*> /. 2)) * N is Element of the carrier of V

[(Y . (<*M,N,SG*> /. 2)),N] is set

{(Y . (<*M,N,SG*> /. 2)),N} is non empty finite set

{{(Y . (<*M,N,SG*> /. 2)),N},{(Y . (<*M,N,SG*> /. 2))}} is non empty finite V42() set

the Mult of V . [(Y . (<*M,N,SG*> /. 2)),N] is set

(V,<*M,N,SG*>,Y) . 1 is set

<*M,N,SG*> /. 1 is Element of the carrier of V

Y . (<*M,N,SG*> /. 1) is complex Element of COMPLEX

(Y . (<*M,N,SG*> /. 1)) * (<*M,N,SG*> /. 1) is Element of the carrier of V

[(Y . (<*M,N,SG*> /. 1)),(<*M,N,SG*> /. 1)] is set

{(Y . (<*M,N,SG*> /. 1)),(<*M,N,SG*> /. 1)} is non empty finite set

{(Y . (<*M,N,SG*> /. 1))} is non empty trivial finite 1 -element V68() set

{{(Y . (<*M,N,SG*> /. 1)),(<*M,N,SG*> /. 1)},{(Y . (<*M,N,SG*> /. 1))}} is non empty finite V42() set

the Mult of V . [(Y . (<*M,N,SG*> /. 1)),(<*M,N,SG*> /. 1)] is set

(Y . (<*M,N,SG*> /. 1)) * M is Element of the carrier of V

[(Y . (<*M,N,SG*> /. 1)),M] is set

{(Y . (<*M,N,SG*> /. 1)),M} is non empty finite set

{{(Y . (<*M,N,SG*> /. 1)),M},{(Y . (<*M,N,SG*> /. 1))}} is non empty finite V42() set

the Mult of V . [(Y . (<*M,N,SG*> /. 1)),M] is set

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed V138() CLSStruct

the carrier of V is non empty set

M is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V)

(V,M) is finite Element of bool the carrier of V

bool the carrier of V is non empty set

{ b

N is Relation-like Function-like FinSequence-like set

rng N is set

SG is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

(V,SG,M) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

Sum (V,SG,M) is Element of the carrier of V

rng SG is Element of bool the carrier of V

N is Element of the carrier of V

SG is Element of the carrier of V

Y is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

rng Y is Element of bool the carrier of V

(V,Y,M) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

Sum (V,Y,M) is Element of the carrier of V

r2 is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

rng r2 is Element of bool the carrier of V

(V,r2,M) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

Sum (V,r2,M) is Element of the carrier of V

len Y is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

len r2 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

dom Y is V68() V69() V70() V71() V72() V73() Element of bool NAT

Seg (len Y) is V68() V69() V70() V71() V72() V73() Element of bool NAT

{ b

dom r2 is V68() V69() V70() V71() V72() V73() Element of bool NAT

Seg (len r2) is V68() V69() V70() V71() V72() V73() Element of bool NAT

{ b

r1 is set

r2 . r1 is set

{(r2 . r1)} is non empty trivial finite 1 -element set

Y " {(r2 . r1)} is V68() V69() V70() V71() V72() V73() Element of bool NAT

r3 is set

{r3} is non empty trivial finite 1 -element set

[:(dom Y),(dom Y):] is RAT -valued INT -valued V58() V59() V60() V61() set

bool [:(dom Y),(dom Y):] is non empty set

r1 is Relation-like dom Y -defined dom Y -valued Function-like total quasi_total V58() V59() V60() V61() Element of bool [:(dom Y),(dom Y):]

rng r1 is V68() V69() V70() V71() V72() V73() Element of bool REAL

r3 is set

Y . r3 is set

r2 is set

r2 . r2 is set

{(r2 . r2)} is non empty trivial finite 1 -element set

Y " {(r2 . r2)} is V68() V69() V70() V71() V72() V73() Element of bool NAT

Im (Y,r3) is set

{r3} is non empty trivial finite 1 -element set

Y .: {r3} is finite set

Y " (Im (Y,r3)) is V68() V69() V70() V71() V72() V73() Element of bool NAT

r1 . r2 is ordinal natural complex real finite cardinal ext-real non negative set

{(r1 . r2)} is non empty trivial finite V42() 1 -element V68() V69() V70() V71() V72() V73() set

dom r1 is V68() V69() V70() V71() V72() V73() Element of bool (dom Y)

bool (dom Y) is non empty set

len (V,Y,M) is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

r2 is set

dom r1 is set

r1 . r2 is ordinal natural complex real finite cardinal ext-real non negative set

r3 is set

r1 . r3 is ordinal natural complex real finite cardinal ext-real non negative set

dom r1 is V68() V69() V70() V71() V72() V73() Element of bool (dom Y)

bool (dom Y) is non empty set

r2 . r2 is set

{(r2 . r2)} is non empty trivial finite 1 -element set

r2 . r3 is set

{(r2 . r3)} is non empty trivial finite 1 -element set

Y " {(r2 . r2)} is V68() V69() V70() V71() V72() V73() Element of bool NAT

{(r1 . r2)} is non empty trivial finite V42() 1 -element V68() V69() V70() V71() V72() V73() set

Y " {(r2 . r3)} is V68() V69() V70() V71() V72() V73() Element of bool NAT

{(r1 . r3)} is non empty trivial finite V42() 1 -element V68() V69() V70() V71() V72() V73() set

dom (V,r2,M) is V68() V69() V70() V71() V72() V73() Element of bool NAT

len (V,r2,M) is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

Seg (len (V,r2,M)) is V68() V69() V70() V71() V72() V73() Element of bool NAT

{ b

dom (V,Y,M) is V68() V69() V70() V71() V72() V73() Element of bool NAT

Seg (len (V,Y,M)) is V68() V69() V70() V71() V72() V73() Element of bool NAT

{ b

[:(dom (V,Y,M)),(dom (V,Y,M)):] is RAT -valued INT -valued V58() V59() V60() V61() set

bool [:(dom (V,Y,M)),(dom (V,Y,M)):] is non empty set

r3 is Relation-like dom Y -defined dom Y -valued Function-like one-to-one total quasi_total onto bijective V58() V59() V60() V61() Element of bool [:(dom Y),(dom Y):]

u2 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

(V,r2,M) . u2 is set

r2 /. u2 is Element of the carrier of V

M . (r2 /. u2) is complex Element of COMPLEX

(M . (r2 /. u2)) * (r2 /. u2) is Element of the carrier of V

the Mult of V is non empty Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]

[:COMPLEX, the carrier of V:] is non empty non trivial non finite set

[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

[(M . (r2 /. u2)),(r2 /. u2)] is set

{(M . (r2 /. u2)),(r2 /. u2)} is non empty finite set

{(M . (r2 /. u2))} is non empty trivial finite 1 -element V68() set

{{(M . (r2 /. u2)),(r2 /. u2)},{(M . (r2 /. u2))}} is non empty finite V42() set

the Mult of V . [(M . (r2 /. u2)),(r2 /. u2)] is set

r2 . u2 is set

r1 is Relation-like dom (V,Y,M) -defined dom (V,Y,M) -valued Function-like one-to-one total quasi_total onto bijective V58() V59() V60() V61() Element of bool [:(dom (V,Y,M)),(dom (V,Y,M)):]

dom r1 is V68() V69() V70() V71() V72() V73() Element of bool (dom (V,Y,M))

bool (dom (V,Y,M)) is non empty set

r1 . u2 is ordinal natural complex real finite cardinal ext-real non negative set

Y . (r1 . u2) is set

{(Y . (r1 . u2))} is non empty trivial finite 1 -element set

Im (Y,(r1 . u2)) is set

{(r1 . u2)} is non empty trivial finite V42() 1 -element V68() V69() V70() V71() V72() V73() set

Y .: {(r1 . u2)} is finite set

{(r2 . u2)} is non empty trivial finite 1 -element set

Y " {(r2 . u2)} is V68() V69() V70() V71() V72() V73() Element of bool NAT

Y .: (Y " {(r2 . u2)}) is Element of bool the carrier of V

y1 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

Y . y1 is set

Y /. y1 is Element of the carrier of V

(V,Y,M) . (r1 . u2) is set

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed V138() CLSStruct

(V) is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V)

the carrier of V is non empty set

(V,(V)) is Element of the carrier of V

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

(V,(V)) is empty proper ordinal natural complex real finite V42() cardinal {} -element ext-real non positive non negative V68() V69() V70() V71() V72() V73() V74() Element of bool the carrier of V

bool the carrier of V is non empty set

{ b

M is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

rng M is Element of bool the carrier of V

(V,M,(V)) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

Sum (V,M,(V)) is Element of the carrier of V

len (V,M,(V)) is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed V138() vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct

the carrier of V is non empty set

bool the carrier of V is non empty set

M is Element of bool the carrier of V

N is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

N + 1 is non empty ordinal natural complex real finite cardinal ext-real positive non negative Element of REAL

SG is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V,M)

(V,SG) is finite Element of bool the carrier of V

{ b

(V,SG) is Element of the carrier of V

Y is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

rng Y is Element of bool the carrier of V

(V,Y,SG) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

Sum (V,Y,SG) is Element of the carrier of V

Seg N is V68() V69() V70() V71() V72() V73() Element of bool NAT

{ b

Y | (Seg N) is Relation-like NAT -defined the carrier of V -valued Function-like Element of bool [:NAT, the carrier of V:]

[:NAT, the carrier of V:] is non trivial non finite set

bool [:NAT, the carrier of V:] is non empty non trivial non finite set

card (V,SG) is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of omega

len Y is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

len (V,Y,SG) is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

Seg (N + 1) is V68() V69() V70() V71() V72() V73() Element of bool NAT

{ b

dom Y is V68() V69() V70() V71() V72() V73() Element of bool NAT

Y . (N + 1) is set

[: the carrier of V,COMPLEX:] is non empty non trivial non finite V58() set

bool [: the carrier of V,COMPLEX:] is non empty non trivial non finite set

r1 is Element of the carrier of V

r3 is non empty Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() Element of bool [: the carrier of V,COMPLEX:]

r3 . r1 is complex Element of COMPLEX

Funcs ( the carrier of V,COMPLEX) is non empty functional FUNCTION_DOMAIN of the carrier of V, COMPLEX

r3 is Element of the carrier of V

SG . r3 is complex Element of COMPLEX

r2 is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() Element of Funcs ( the carrier of V,COMPLEX)

r2 . r3 is complex Element of COMPLEX

r3 is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V)

(V,r3) is finite Element of bool the carrier of V

{ b

{r1} is non empty trivial finite 1 -element Element of bool the carrier of V

(V,SG) \ {r1} is finite Element of bool the carrier of V

r1 is set

r3 . r1 is complex set

SG . r1 is complex set

u2 is Element of the carrier of V

r3 . u2 is complex Element of COMPLEX

u2 is Element of the carrier of V

r3 . u2 is complex Element of COMPLEX

u2 is Element of the carrier of V

r3 . u2 is complex Element of COMPLEX

r1 is set

SG . r1 is complex set

r3 . r1 is complex set

u2 is Element of the carrier of V

SG . u2 is complex Element of COMPLEX

M \ {r1} is Element of bool the carrier of V

r2 is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

len r2 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

r1 is Relation-like the carrier of V -defined COMPLEX -valued Function-like total quasi_total V58() (V,M)

(V,r2,r1) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

len (V,r2,r1) is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

rng r2 is Element of bool the carrier of V

(V,r1) is finite Element of bool the carrier of V

{ b

u2 is set

dom r2 is V68() V69() V70() V71() V72() V73() Element of bool NAT

y1 is set

r2 . y1 is set

x1 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT

r2 . x1 is set

Y . x1 is set

u2 is set

y1 is set

Y . y1 is set

(dom Y) \ (Seg N) is V68() V69() V70() V71() V72() V73() Element of bool NAT

(Seg (N + 1)) \ (Seg N) is V68() V69() V70() V71() V72() V73() Element of bool NAT

{(N + 1)} is non empty trivial finite V42() 1 -element V68() V69() V70() V71() V72() V73() Element of bool REAL

(dom Y) /\ (Seg N) is V68() V69() V70() V71() V72() V73() Element of bool NAT

dom r2 is V68() V69() V70() V71() V72() V73() Element of bool NAT

r2 . y1 is set

(Seg (N + 1)) /\ (Seg N) is V68() V69() V70() V71() V72() V73() Element of bool NAT

dom (V,r2,r1) is V68() V69() V70() V71() V72() V73() Element of bool NAT

dom (V,Y,SG) is V68() V69() V70() V71() V72() V73() Element of bool NAT

(dom (V,Y,SG)) /\ (Seg N) is V68() V69() V70() V71() V72() V73() Element of bool NAT

u2 is set

dom r2 is V68() V69() V70() V71() V72() V73() Element of bool NAT

r2 . u2 is set

Y . u2 is set

y1 is Element of the carrier of V

(V,r2,r1) . u2 is set

r1 . y1 is complex Element of COMPLEX

(r1 . y1) * y1 is Element of the carrier of V

the Mult of V is non empty Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]

[:COMPLEX, the carrier of V:] is non empty non trivial non finite set

[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty non trivial non finite set

[(r1 . y1),y1] is set

{(r1 . y1),y1} is non empty finite set

{(r1 . y1)} is non empty trivial finite 1 -element V68() set

{{(r1 . y1),y1},{(r1 . y1)}} is non empty finite V42() set

the Mult of V . [(r1 . y1),y1] is set

SG . y1 is complex Element of COMPLEX

(SG . y1) * y1 is Element of the carrier of V

[(SG . y1),y1] is set

{(SG . y1),y1} is non empty finite set

{(SG . y1)} is non empty trivial finite 1 -element V68() set

{{(SG . y1),y1},{(SG . y1)}} is non empty finite V42() set

the Mult of V . [(SG . y1),y1] is set

(V,Y,SG) . u2 is set

(V,Y,SG) | (Seg N) is Relation-like NAT -defined the carrier of V -valued Function-like Element of bool [:NAT, the carrier of V:]

card (V,r1) is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of omega

card {r1} is non empty ordinal natural complex real finite cardinal V49() V50() ext-real positive non negative V68() V69() V70() V71() V72() V73() Element of omega

(N + 1) - (card {r1}) is complex real ext-real Element of REAL

- (card {r1}) is non empty complex real ext-real non positive negative set

(N + 1) + (- (card {r1})) is complex real ext-real set

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

- 1 is non empty complex real ext-real non positive negative set

(N + 1) + (- 1) is complex real ext-real set

(V,r1) is Element of the carrier of V

SG . r1 is complex Element of COMPLEX

(SG . r1) * r1 is Element of the carrier of V

[(SG . r1),r1] is set

{(SG . r1),r1} is non empty finite set

{(SG . r1)} is non empty trivial finite 1 -element V68() set

{{(SG . r1),r1},{(SG . r1)}} is non empty finite V42() set

the Mult of V . [(SG . r1),r1] is set

Sum (V,r2,r1) is Element of the carrier of V

Seg (len (V,r2,r1)) is V68() V69() V70() V71() V72() V73() Element of bool NAT

{ b

(V,Y,SG) . (len Y) is set

(Sum (V,r2,r1)) + ((SG . r1) * r1) is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like total quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

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

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

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

the addF of V . ((Sum (V,r2,r1)),((SG . r1) * r1)) is Element of the carrier of V

[(Sum (V,r2,r1)),((SG . r1) * r1)] is set

{(Sum (V,r2,r1)),((SG . r1) * r1)} is non empty finite set

{(Sum (V,r2,r1))} is non empty trivial finite 1 -element set