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
{ b1 where b1 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{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
{ b1 where b1 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{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
{ b1 where b1 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b1 & b1 <= 3 ) } is set
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
{ b1 where b1 is Element of the carrier of V : not M . b1 = 0c } is set
N is Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not M . b1 = {} } is set
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
{ b1 where b1 is Element of the carrier of V : not M . b1 = 0c } is set
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
{ b1 where b1 is Element of the carrier of V : not M . b1 = 0c } is set
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
{ b1 where b1 is Element of the carrier of V : not N . b1 = 0c } is set
the Element of { b1 where b1 is Element of the carrier of V : not N . b1 = 0c } is Element of { b1 where b1 is Element of the carrier of V : not N . b1 = 0c }
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
{ b1 where b1 is Element of the carrier of V : not M . b1 = 0c } is set
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
{ b1 where b1 is Element of the carrier of V : not N . b1 = 0c } is set
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
{ b1 where b1 is Element of the carrier of V : not (V) . b1 = 0c } is set
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
{ b1 where b1 is Element of the carrier of V : not (V) . b1 = 0c } is set
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
{ b1 where b1 is Element of the carrier of V : not N . b1 = 0c } is set
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
{ b1 where b1 is Element of the carrier of V : not SG . b1 = 0c } is set
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
{ b1 where b1 is Element of the carrier of V : not (V) . b1 = 0c } is set
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
{ b1 where b1 is Element of the carrier of V : not M . b1 = 0c } 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 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
{ b1 where b1 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b1 & b1 <= len SG ) } is set
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
{ b1 where b1 is Element of the carrier of V : not M . b1 = 0c } is set
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
{ b1 where b1 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b1 & b1 <= len Y ) } is set
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
{ b1 where b1 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b1 & b1 <= len r2 ) } is set
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
{ b1 where b1 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b1 & b1 <= len (V,r2,M) ) } is set
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
{ b1 where b1 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b1 & b1 <= len (V,Y,M) ) } is set
[:(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
{ b1 where b1 is Element of the carrier of V : not (V) . b1 = 0c } is set
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
{ b1 where b1 is Element of the carrier of V : not SG . b1 = 0c } is set
(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
{ b1 where b1 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b1 & b1 <= N ) } is set
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
{ b1 where b1 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b1 & b1 <= N + 1 ) } is set
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
{ b1 where b1 is Element of the carrier of V : not r3 . b1 = 0c } is set
{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
{ b1 where b1 is Element of the carrier of V : not r1 . b1 = 0c } is set
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
{ b1 where b1 is ordinal natural complex real finite cardinal V49() V50() ext-real non negative V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b1 & b1 <= len (V,r2,r1) ) } is set
(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