:: MATRIX_5 semantic presentation

REAL is non zero V33() set

K19(REAL) is set

the U1 of F_Complex is non zero V12() set
COMPLEX is non zero V33() set

K19(omega) is set
K19(NAT) is set

RAT is non zero V33() set
INT is non zero V33() set
K20(COMPLEX,COMPLEX) is set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(REAL,REAL) is set
K19(K20(REAL,REAL)) is set
K20(K20(REAL,REAL),REAL) is set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is set
K20(K20(NAT,NAT),NAT) is set
K19(K20(K20(NAT,NAT),NAT)) is set
0 is set

Seg 1 is Element of K19(NAT)

0. F_Complex is complex zero Element of the U1 of F_Complex
1_ F_Complex is complex Element of the U1 of F_Complex
K138(F_Complex) is complex non zero Element of the U1 of F_Complex
K176(COMPLEX) is M10( COMPLEX )

K176( the U1 of F_Complex) is M10( the U1 of F_Complex)

(i) + (- (j)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)

i is complex set

M1 is complex Element of the U1 of F_Complex

q0 is complex Element of the U1 of F_Complex

M1 is complex Element of the U1 of F_Complex

the U1 of i is non zero V12() set
K176( the U1 of i) is M10( the U1 of i)
1_ i is Element of the U1 of i
K138(i) is non zero Element of the U1 of i
j is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
(1_ i) * j is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
Indices j is set

[M1,M2] is set
((1_ i) * j) * (M1,M2) is Element of the U1 of i
j * (M1,M2) is Element of the U1 of i
(1_ i) * (j * (M1,M2)) is Element of the U1 of i

the U1 of i is non zero V12() set
K176( the U1 of i) is M10( the U1 of i)
M1 is Element of the U1 of i
j is Element of the U1 of i
j * M1 is Element of the U1 of i
M2 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
M1 * M2 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
j * (M1 * M2) is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
(j * M1) * M2 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)

Indices (j * (M1 * M2)) is set

[q0,i2] is set
(j * (M1 * M2)) * (q0,i2) is Element of the U1 of i
((j * M1) * M2) * (q0,i2) is Element of the U1 of i
Indices (M1 * M2) is set
Indices M2 is set
(M1 * M2) * (q0,i2) is Element of the U1 of i
j * ((M1 * M2) * (q0,i2)) is Element of the U1 of i
M2 * (q0,i2) is Element of the U1 of i
M1 * (M2 * (q0,i2)) is Element of the U1 of i
j * (M1 * (M2 * (q0,i2))) is Element of the U1 of i
(j * M1) * (M2 * (q0,i2)) is Element of the U1 of i

the U1 of i is non zero V12() set
K176( the U1 of i) is M10( the U1 of i)
j is Element of the U1 of i
M1 is Element of the U1 of i
j + M1 is Element of the U1 of i
M2 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
(j + M1) * M2 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
j * M2 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
M1 * M2 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
(j * M2) + (M1 * M2) is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)

Indices ((j + M1) * M2) is set

[q0,i2] is set
((j + M1) * M2) * (q0,i2) is Element of the U1 of i
((j * M2) + (M1 * M2)) * (q0,i2) is Element of the U1 of i
Indices M2 is set
Indices (j * M2) is set
(j * M2) * (q0,i2) is Element of the U1 of i
(M1 * M2) * (q0,i2) is Element of the U1 of i
((j * M2) * (q0,i2)) + ((M1 * M2) * (q0,i2)) is Element of the U1 of i
M2 * (q0,i2) is Element of the U1 of i
j * (M2 * (q0,i2)) is Element of the U1 of i
(j * (M2 * (q0,i2))) + ((M1 * M2) * (q0,i2)) is Element of the U1 of i
M1 * (M2 * (q0,i2)) is Element of the U1 of i
(j * (M2 * (q0,i2))) + (M1 * (M2 * (q0,i2))) is Element of the U1 of i
(j + M1) * (M2 * (q0,i2)) is Element of the U1 of i
len ((j * M2) + (M1 * M2)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width ((j * M2) + (M1 * M2)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
() + () is complex Element of the U1 of F_Complex

i is complex Element of the U1 of F_Complex

() + () is complex Element of the U1 of F_Complex

(() + ()) + () is complex Element of the U1 of F_Complex
(() + ()) + () is complex Element of COMPLEX

(M1) + (M1) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)

((M1,M1)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
((M1,M1)) + (M1) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
((((M1,M1)) + (M1))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)

the addF of F_Complex is Relation-like K20( the U1 of F_Complex, the U1 of F_Complex) -defined the U1 of F_Complex -valued Function-like V18(K20( the U1 of F_Complex, the U1 of F_Complex), the U1 of F_Complex) Element of K19(K20(K20( the U1 of F_Complex, the U1 of F_Complex), the U1 of F_Complex))
K20( the U1 of F_Complex, the U1 of F_Complex) is set
K20(K20( the U1 of F_Complex, the U1 of F_Complex), the U1 of F_Complex) is set
K19(K20(K20( the U1 of F_Complex, the U1 of F_Complex), the U1 of F_Complex)) is set
the addF of F_Complex . ((),()) is complex Element of the U1 of F_Complex

the addF of F_Complex . ((() + ()),()) is complex Element of the U1 of F_Complex
addcomplex . ((1 + 1),1) is set

i + 1 is complex Element of COMPLEX
j is complex Element of the U1 of F_Complex

(() + ()) * (M1) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(() * (M1)) + ((() + ()) * (M1)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(((() * (M1)) + ((() + ()) * (M1)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(M1) + ((() + ()) * (M1)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(((M1) + ((() + ()) * (M1)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(() * (M1)) + (() * (M1)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(M1) + ((() * (M1)) + (() * (M1))) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(((M1) + ((() * (M1)) + (() * (M1))))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(M1) + (() * (M1)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(M1) + ((M1) + (() * (M1))) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(((M1) + ((M1) + (() * (M1))))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(M1) + ((M1) + (M1)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(((M1) + ((M1) + (M1)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
((M1) + (M1)) + (M1) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
((((M1) + (M1)) + (M1))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)

0. (F_Complex,i,j) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular Matrix of i,j, the U1 of F_Complex

0. (F_Complex,i,j) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular Matrix of i,j, the U1 of F_Complex

((i,j)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)

0. (F_Complex,(len i),()) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular Matrix of len i, width i, the U1 of F_Complex

((i,j)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)

((i,j)) + ((i)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
((((i,j)) + ((i)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)

((j) + (i)) - (i) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
((j) + (i)) + (- (i)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
((((j) + (i)) - (i))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)

0. (F_Complex,(len i),()) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular Matrix of len i, width i, the U1 of F_Complex

(((len i),())) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(i) - (- (j)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)

(i) + (- (- (j))) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)

(j) + (- (i)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)

0. (F_Complex,(len i),()) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular Matrix of len i, width i, the U1 of F_Complex

0. (F_Complex,(len i),()) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular Matrix of len i, width i, the U1 of F_Complex

(((len i),())) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(i) + (((len i),())) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(((i) + (((len i),())))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)

- (((len i),())) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)

((((len i),()))) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(i) + ((((len i),()))) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(((i) + ((((len i),()))))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)

(i) + (- (i)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(i) - ((i) - (i)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
- ((i) - (i)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(i) + (- ((i) - (i))) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(((i) - ((i) - (i)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)

the U1 of i is non zero V12() set
K176( the U1 of i) is M10( the U1 of i)
j is Element of the U1 of i
M1 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)

M2 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)

M1 + M2 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
j * (M1 + M2) is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
j * M1 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
j * M2 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
(j * M1) + (j * M2) is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)

Indices (j * (M1 + M2)) is set

[q0,i2] is set
(j * (M1 + M2)) * (q0,i2) is Element of the U1 of i
((j * M1) + (j * M2)) * (q0,i2) is Element of the U1 of i
Indices M2 is set
Indices M1 is set
Indices (M1 + M2) is set
Indices (j * M1) is set
(j * M1) * (q0,i2) is Element of the U1 of i
(j * M2) * (q0,i2) is Element of the U1 of i
((j * M1) * (q0,i2)) + ((j * M2) * (q0,i2)) is Element of the U1 of i
M1 * (q0,i2) is Element of the U1 of i
j * (M1 * (q0,i2)) is Element of the U1 of i
(j * (M1 * (q0,i2))) + ((j * M2) * (q0,i2)) is Element of the U1 of i
M2 * (q0,i2) is Element of the U1 of i
j * (M2 * (q0,i2)) is Element of the U1 of i
(j * (M1 * (q0,i2))) + (j * (M2 * (q0,i2))) is Element of the U1 of i
(M1 * (q0,i2)) + (M2 * (q0,i2)) is Element of the U1 of i
j * ((M1 * (q0,i2)) + (M2 * (q0,i2))) is Element of the U1 of i
(M1 + M2) * (q0,i2) is Element of the U1 of i
j * ((M1 + M2) * (q0,i2)) is Element of the U1 of i
len ((j * M1) + (j * M2)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width ((j * M1) + (j * M2)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT

M1 is complex set

((M1,i)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
((M1,j)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
((M1,i)) + ((M1,j)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
((((M1,i)) + ((M1,j)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
M2 is complex Element of the U1 of F_Complex

(((M2 * (i)))) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(((M2 * (i)))) + ((M1,j)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(((((M2 * (i)))) + ((M1,j)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)

(((M2 * (j)))) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(M2 * (i)) + (((M2 * (j)))) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(((M2 * (i)) + (((M2 * (j)))))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(M2 * (i)) + (M2 * (j)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(((M2 * (i)) + (M2 * (j)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
((i,j)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
M2 * ((i,j)) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)

the U1 of i is non zero V12() set
K176( the U1 of i) is M10( the U1 of i)
j is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)

M1 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)

0. (i,(len j),()) is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular Matrix of len j, width j, the U1 of i
(0. (i,(len j),())) * M1 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)

0. (i,(len j),(width M1)) is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular Matrix of len j, width M1, the U1 of i

len ((0. (i,(len j),())) * M1) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width ((0. (i,(len j),())) * M1) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
- ((0. (i,(len j),())) * M1) is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
width (- ((0. (i,(len j),())) * M1)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(0. (i,(len j),())) + (0. (i,(len j),())) is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
((0. (i,(len j),())) + (0. (i,(len j),()))) * M1 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
((0. (i,(len j),())) * M1) + ((0. (i,(len j),())) * M1) is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
len (- ((0. (i,(len j),())) * M1)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(((0. (i,(len j),())) * M1) + ((0. (i,(len j),())) * M1)) + (- ((0. (i,(len j),())) * M1)) is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
((0. (i,(len j),())) * M1) - ((0. (i,(len j),())) * M1) is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
((0. (i,(len j),())) * M1) + (- ((0. (i,(len j),())) * M1)) is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
((0. (i,(len j),())) * M1) + (((0. (i,(len j),())) * M1) - ((0. (i,(len j),())) * M1)) is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)

0. (F_Complex,(len i),()) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular Matrix of len i, width i, the U1 of F_Complex

(((len i),())) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)

(((len i),())) * (j) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of F_Complex)
(((((len i),())) * (j))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)

0. (F_Complex,(len i),()) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular Matrix of len i, width j, the U1 of F_Complex

the U1 of i is non zero V12() set
K176( the U1 of i) is M10( the U1 of i)
0. i is zero Element of the U1 of i
j is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)

(0. i) * j is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)

0. (i,(len j),()) is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular Matrix of len j, width j, the U1 of i

Indices (0. (i,(len j),())) is set

[M1,M2] is set
((0. i) * j) * (M1,M2) is Element of the U1 of i
(0. (i,(len j),())) * (M1,M2) is Element of the U1 of i
Indices j is set
j * (M1,M2) is Element of the U1 of i
(0. i) * (j * (M1,M2)) is Element of the U1 of i

0. (F_Complex,(len j),()) is Relation-like NAT -defined K176( the U1 of F_Complex) -valued Function-like FinSequence-like tabular Matrix of len j, width j, the U1 of F_Complex

i is complex Element of the U1 of F_Complex

j is set
i . j is set
dom i is set
rng i is set
dom i is set
dom i is set

M1 * (i,1) is complex Element of COMPLEX
M2 * (1,j) is complex Element of COMPLEX
(M1 * (i,1)) * (M2 * (1,j)) is complex Element of COMPLEX
<*((M1 * (i,1)) * (M2 * (1,j)))*> is Relation-like NAT -defined COMPLEX -valued Function-like FinSequence-like complex-valued FinSequence of COMPLEX

(<*((M1 * (i,1)) * (M2 * (1,j)))*>,(i2 + 1)) is complex Element of COMPLEX
(<*((M1 * (i,1)) * (M2 * (1,j)))*>,i2) is complex Element of COMPLEX
M1 * (i,(i2 + 1)) is complex Element of COMPLEX
M2 * ((i2 + 1),j) is complex Element of COMPLEX
(M1 * (i,(i2 + 1))) * (M2 * ((i2 + 1),j)) is complex Element of COMPLEX
(<*((M1 * (i,1)) * (M2 * (1,j)))*>,i2) + ((M1 * (i,(i2 + 1))) * (M2 * ((i2 + 1),j))) is complex Element of COMPLEX

(q2,1) is complex Element of COMPLEX

(q2,1) is complex Element of COMPLEX
(q2,(i2 + 1)) is complex Element of COMPLEX
M1 * (i,((i2 + 1) + 1)) is complex Element of COMPLEX
M2 * (((i2 + 1) + 1),j) is complex Element of COMPLEX
(M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j)) is complex Element of COMPLEX
(q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))) is complex Element of COMPLEX
<*((q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*> is Relation-like NAT -defined COMPLEX -valued Function-like FinSequence-like complex-valued FinSequence of COMPLEX
q2 ^ <*((q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*> is Relation-like NAT -defined COMPLEX -valued Function-like FinSequence-like complex-valued FinSequence of COMPLEX
len (q2 ^ <*((q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
((q2 ^ <*((q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>),1) is complex Element of COMPLEX
len <*((q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*> is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(len q2) + (len <*((q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT

((q2 ^ <*((q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>),(k2 + 1)) is complex Element of COMPLEX
((q2 ^ <*((q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>),k2) is complex Element of COMPLEX
M1 * (i,(k2 + 1)) is complex Element of COMPLEX
M2 * ((k2 + 1),j) is complex Element of COMPLEX
(M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j)) is complex Element of COMPLEX
((q2 ^ <*((q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>),k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) is complex Element of COMPLEX

dom q2 is Element of K19(NAT)
(q2,k2) is complex Element of COMPLEX
(q2,(k2 + 1)) is complex Element of COMPLEX

dom q2 is Element of K19(NAT)
(q2,k2) is complex Element of COMPLEX
(<*((q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>,1) is complex Element of COMPLEX
dom <*((q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*> is Element of K19(NAT)

dom q2 is Element of K19(NAT)

((q2 ^ <*((q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>),(k2 + 1)) is complex Element of COMPLEX
((q2 ^ <*((q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>),k2) is complex Element of COMPLEX
M1 * (i,(k2 + 1)) is complex Element of COMPLEX
M2 * ((k2 + 1),j) is complex Element of COMPLEX
(M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j)) is complex Element of COMPLEX
((q2 ^ <*((q2,(i2 + 1)) + ((M1 * (i,((i2 + 1) + 1))) * (M2 * (((i2 + 1) + 1),j))))*>),k2) + ((M1 * (i,(k2 + 1))) * (M2 * ((k2 + 1),j))) is complex Element of COMPLEX
len <*((M1 * (i,1)) * (M2 * (1,j)))*> is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(<*((M1 * (i,1)) * (M2 * (1,j)))*>,1) is complex Element of COMPLEX

(0 + 1) - 1 is complex V32() ext-real Element of REAL
(len M2) - 1 is complex V32() ext-real Element of REAL