REAL is non zero V33() set
NAT is non zero epsilon-transitive epsilon-connected ordinal Element of K19(REAL)
K19(REAL) is set
F_Complex is V42() V46() V47() right_complementable almost_left_invertible strict unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital doubleLoopStr
the U1 of F_Complex is non zero V12() set
COMPLEX is non zero V33() set
omega is non zero epsilon-transitive epsilon-connected ordinal set
K19(omega) is set
K19(NAT) is set
1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
2 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
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
0 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
Seg 1 is Element of K19(NAT)
addcomplex is Relation-like K20(COMPLEX,COMPLEX) -defined COMPLEX -valued Function-like V18(K20(COMPLEX,COMPLEX), COMPLEX ) Element of K19(K20(K20(COMPLEX,COMPLEX),COMPLEX))
multcomplex is Relation-like K20(COMPLEX,COMPLEX) -defined COMPLEX -valued Function-like V18(K20(COMPLEX,COMPLEX), COMPLEX ) Element of K19(K20(K20(COMPLEX,COMPLEX),COMPLEX))
1r is complex Element of COMPLEX
0c is complex Element of COMPLEX
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 )
i is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
K176( the U1 of F_Complex) is M10( the U1 of F_Complex)
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 is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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 is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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 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 Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
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) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
i is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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)) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
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) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
((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 is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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 is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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)
(((i) + (j))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
i is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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) 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 Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
i is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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 is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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) 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(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)
(((i) * (j))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
i is complex set
j is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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 is complex Element of 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 * (j))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
q0 is complex Element of the U1 of F_Complex
q0 * (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)
((q0 * (j))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
M2 is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
q0 is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
M1 is complex Element of 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 * (j))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
i is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(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 epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
j is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
width j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(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)
width (j) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
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 epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(i) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len (i) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
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)
width j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(j) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
width (j) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
i is V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital doubleLoopStr
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 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real set
M2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real 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
len ((1_ i) * j) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
len j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width ((1_ i) * j) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
j is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(1,j) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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)
(1_ F_Complex) * (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)
(((1_ F_Complex) * (j))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
i is V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital doubleLoopStr
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)
len ((j * M1) * M2) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
len M2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width ((j * M1) * M2) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width M2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
len (j * (M1 * M2)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
len (M1 * M2) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width (j * (M1 * M2)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width (M1 * M2) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
Indices (j * (M1 * M2)) is set
q0 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real set
i2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real 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
i is V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital doubleLoopStr
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)
len (j * M2) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
len M2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width (j * M2) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width M2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
len ((j + M1) * M2) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width ((j + M1) * M2) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
Indices ((j + M1) * M2) is set
q0 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real set
i2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real 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
(1_ F_Complex) + (1_ F_Complex) is complex Element of the U1 of F_Complex
(1_ F_Complex) + (1_ F_Complex) is complex Element of COMPLEX
j is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(j,j) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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) + (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) + (j))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(2,j) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(1_ F_Complex) * (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 Element of 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(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
3 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(1_ F_Complex) + (1_ F_Complex) is complex Element of the U1 of F_Complex
(1_ F_Complex) + (1_ F_Complex) is complex Element of COMPLEX
((1_ F_Complex) + (1_ F_Complex)) + (1_ F_Complex) is complex Element of the U1 of F_Complex
((1_ F_Complex) + (1_ F_Complex)) + (1_ F_Complex) is complex Element of COMPLEX
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(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(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),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)
(3,M1) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len M1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
len (M1) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width M1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width (M1) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
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 . ((1_ F_Complex),(1_ F_Complex)) is complex Element of the U1 of F_Complex
addcomplex . (1r,1r) is complex Element of COMPLEX
the addF of F_Complex . (((1_ F_Complex) + (1_ F_Complex)),(1_ F_Complex)) is complex Element of the U1 of F_Complex
addcomplex . ((1 + 1),1) is set
i is complex Element of COMPLEX
i + 1 is complex Element of COMPLEX
j is complex Element of the U1 of F_Complex
j * (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)
((j * (M1))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(1_ 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)
((1_ F_Complex) + (1_ 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)
((1_ F_Complex) * (M1)) + (((1_ F_Complex) + (1_ 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)
((((1_ F_Complex) * (M1)) + (((1_ F_Complex) + (1_ F_Complex)) * (M1)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(M1) + (((1_ F_Complex) + (1_ 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) + (((1_ F_Complex) + (1_ F_Complex)) * (M1)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
((1_ F_Complex) * (M1)) + ((1_ 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) + (((1_ F_Complex) * (M1)) + ((1_ 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) + (((1_ F_Complex) * (M1)) + ((1_ F_Complex) * (M1))))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(M1) + ((1_ 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) + ((1_ 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) + ((1_ F_Complex) * (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)
i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real set
j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real set
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(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(i,j) 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(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)
i is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
j is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(i,j) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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) 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(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
((len i),(width i)) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
0. (F_Complex,(len i),(width 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),(width i)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(i) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
- (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))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
((i,j),(i)) 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)
((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( 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) 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( 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)
i is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
j is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(i,j) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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) 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(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
((len i),(width i)) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
0. (F_Complex,(len i),(width 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),(width i)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(i) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
- (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))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(j) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
- (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))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len (j) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width (j) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(((len i),(width 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)
- (- (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)
i is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
j is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(j,i) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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 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)
- (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)) 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(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
((len i),(width i)) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
0. (F_Complex,(len i),(width 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),(width i)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(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)
i is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
((len i),(width i)) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
0. (F_Complex,(len i),(width 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),(width i)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(i,((len i),(width i))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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),(width 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),(width 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),(width i))))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len (i) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width (i) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(((len i),(width i))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
- (((len i),(width 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),(width i))))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(i,(((len i),(width i)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
((((len i),(width 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),(width 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),(width 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) 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)) 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)
i is V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital doubleLoopStr
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)
len M1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
M2 is Relation-like NAT -defined K176( the U1 of i) -valued Function-like FinSequence-like tabular FinSequence of K176( the U1 of i)
len M2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width M1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width M2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
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)
len (j * (M1 + M2)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
len (M1 + M2) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width (j * (M1 + M2)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width (M1 + M2) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
len (j * M1) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width (j * M1) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
Indices (j * (M1 + M2)) is set
q0 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real set
i2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real 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
i is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
j is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(i,j) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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) 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(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
M1 is complex set
(M1,(i,j)) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(M1,i) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(M1,j) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
((M1,i),(M1,j)) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
((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))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(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 * (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)
((M2 * ((i,j)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
i is V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital doubleLoopStr
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)
width j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
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 M1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
len j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
0. (i,(len j),(width 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),(width 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 M1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
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),(width j))) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width (0. (i,(len j),(width j))) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
len ((0. (i,(len j),(width j))) * M1) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width ((0. (i,(len j),(width j))) * M1) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
- ((0. (i,(len j),(width 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),(width j))) * M1)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(0. (i,(len j),(width j))) + (0. (i,(len j),(width 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),(width j))) + (0. (i,(len j),(width 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 j))) * M1) + ((0. (i,(len j),(width 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),(width j))) * M1)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(((0. (i,(len j),(width j))) * M1) + ((0. (i,(len j),(width j))) * M1)) + (- ((0. (i,(len j),(width 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 j))) * M1) - ((0. (i,(len j),(width 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 j))) * M1) + (- ((0. (i,(len j),(width 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 j))) * M1) + (((0. (i,(len j),(width j))) * M1) - ((0. (i,(len j),(width 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)
i is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
width i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
j is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
len i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
((len i),(width i)) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
0. (F_Complex,(len i),(width 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),(width i)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(((len i),(width i)),j) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(((len i),(width 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) 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),(width 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),(width i))) * (j))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
width j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
((len i),(width j)) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
0. (F_Complex,(len i),(width j)) 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
((0. (F_Complex,(len i),(width j)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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 epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
i is V42() V46() V47() right_complementable almost_left_invertible unital V117() V119() V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital doubleLoopStr
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)
len j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(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)
width j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
0. (i,(len j),(width 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
len (0. (i,(len j),(width j))) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width (0. (i,(len j),(width j))) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
Indices (0. (i,(len j),(width j))) is set
M1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real set
M2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real set
[M1,M2] is set
((0. i) * j) * (M1,M2) is Element of the U1 of i
(0. (i,(len j),(width 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
len ((0. i) * j) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
width ((0. i) * j) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
j is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(0,j) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
width j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
((len j),(width j)) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
0. (F_Complex,(len j),(width 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
((0. (F_Complex,(len j),(width j)))) is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
(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 Element of 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(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
i is Relation-like Function-like complex-valued set
j is set
i . j is set
dom i is set
rng i is set
dom i is set
dom i is set
i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
M2 is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
len M2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
M1 is Relation-like NAT -defined K176(COMPLEX) -valued Function-like FinSequence-like tabular FinSequence of K176(COMPLEX)
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
i2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
i2 + 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(<*((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
i2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
i2 + 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(i2 + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
q2 is Relation-like NAT -defined COMPLEX -valued Function-like FinSequence-like complex-valued FinSequence of COMPLEX
len q2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(q2,1) is complex Element of COMPLEX
q2 is Relation-like NAT -defined COMPLEX -valued Function-like FinSequence-like complex-valued FinSequence of COMPLEX
len q2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(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
k2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
k2 + 1 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
(len q2) + 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
dom q2 is Element of K19(NAT)
(q2,k2) is complex Element of COMPLEX
(q2,(k2 + 1)) is complex Element of COMPLEX
(len q2) + 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
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)
(len q2) + 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
dom q2 is Element of K19(NAT)
k2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
k2 + 1 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
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 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT
(0 + 1) - 1 is complex V32() ext-real Element of REAL
(len M2) - 1 is complex V32() ext-real Element of REAL
(len M2) -' 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative Element of NAT
((len M2) -' 1) + 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real Element of NAT