:: MATRIX_8 semantic presentation

K93() is set

K97() is V11() V24() V25() V26() M2( bool K93())

bool K93() is set

K92() is V11() V24() V25() V26() set

bool K92() is set

bool K97() is set

1 is V11() V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

2 is V11() V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

0 is set

0 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric Matrix of n,n, the U1 of K

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

(1. (K,n)) * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

K181(n, the U1 of K) is M8( the U1 of K)

0. K is V55(K) M2( the U1 of K)

K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))

K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))

K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))

0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

width (0. (K,n,n)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len (0. (K,n,n)) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

(0. (K,n,n)) * (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric Matrix of n,n, the U1 of K

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

K181(n, the U1 of K) is M8( the U1 of K)

0. K is V55(K) M2( the U1 of K)

K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))

K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))

K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

(M1 @) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

width (M1 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len (M1 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

(M1 @) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 @) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 @) * (M1 @)) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 @) @) * ((M1 @) @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * ((M1 @) @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K

K181(n, the U1 of K) is M8( the U1 of K)

0. K is V55(K) M2( the U1 of K)

K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))

K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))

K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 + M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 + M2) * (M1 + M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M1) + (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) + (0. (K,n))) + (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(((M1 * M1) + (0. (K,n))) + (0. (K,n))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) + (0. (K,n))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

- (M2 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 + M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

len (M1 * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (M1 * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

(M1 * M1) + (M2 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

len ((M1 * M1) + (M2 * M1)) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width ((M1 * M1) + (M2 * M1)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len (M2 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (M2 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len (M1 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (M1 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len (M1 + M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (M1 + M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

(M1 + M2) * (M1 + M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 + M2) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 + M2) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 + M2) * M1) + ((M1 + M2) * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) + (M2 * M1)) + ((M1 + M2) * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M2) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) + (M2 * M1)) + ((M1 * M2) + (M2 * M2)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) + (M2 * M1)) + (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(((M1 * M1) + (M2 * M1)) + (M1 * M2)) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 * M1) + (- (M2 * M1)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M1) + ((M2 * M1) + (- (M2 * M1))) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) + ((M2 * M1) + (- (M2 * M1)))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

K181(n, the U1 of K) is M8( the U1 of K)

0. K is V55(K) M2( the U1 of K)

K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))

K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))

K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))

(M1 * M1) + (0. (K,n,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) + (0. (K,n,n))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 + M2) * (M1 + M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 ~) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M2 ~) * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

len (M1 * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (((M2 ~) * M1) * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len (M2 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width ((M2 ~) * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

width (M2 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

(((M2 ~) * M1) * M2) * (((M2 ~) * M1) * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 ~) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(((M2 ~) * M1) * M2) * ((M2 ~) * (M1 * M2)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(((M2 ~) * M1) * M2) * (M2 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((((M2 ~) * M1) * M2) * (M2 ~)) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * (M2 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M2 ~) * M1) * (M2 * (M2 ~)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(((M2 ~) * M1) * (M2 * (M2 ~))) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K

((M2 ~) * M1) * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(((M2 ~) * M1) * (1. (K,n))) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M2 ~) * M1) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M2 ~) * M1) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(((M2 ~) * M1) * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 ~) * (M1 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M2 ~) * (M1 * M1)) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M1) ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 ~) * (M1 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

M1 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

width (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 ~) * (M1 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 ~) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 ~) * M1) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(1. (K,n)) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (M1 * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

(M1 * M2) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M2) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M2) * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * (M2 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * (M2 * M1)) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * (M1 * M2)) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) * M2) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M2) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 @) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

len (M1 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (M2 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

width (M1 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len (M2 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width ((M1 @) * (M2 @)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

((M1 @) * (M2 @)) * ((M1 @) * (M2 @)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 @) * (M2 @)) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(((M1 @) * (M2 @)) * (M1 @)) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 @) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 @) * ((M2 @) * (M1 @)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 @) * ((M2 @) * (M1 @))) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M2) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 @) * ((M1 * M2) @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 @) * ((M1 * M2) @)) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 @) * ((M2 * M1) @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 @) * ((M2 * M1) @)) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 @) * ((M1 @) * (M2 @)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 @) * ((M1 @) * (M2 @))) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 @) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 @) * (M1 @)) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(((M1 @) * (M1 @)) * (M2 @)) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) @) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(((M1 * M1) @) * (M2 @)) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 @) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 @) * ((M2 @) * (M2 @)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 * M2) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 @) * ((M2 * M2) @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 @) * (M2 @)) * ((M1 @) * (M2 @)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (M2 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

(M2 * M1) * (M2 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M2 * M1) * M2) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 * (1. (K,n))) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

(M1 * (M1 @)) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 @) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * (M1 @)) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 @) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

((M1 @) * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 @) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 @) * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

len M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K

(1. (K,n)) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 ~) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 ~) * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 ~) * (M1 * M3) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 ~) * M1) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(1. (K,n)) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M3 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K

M2 * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * (M1 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * (M1 * (M1 ~)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M3 * M1) * (M1 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M3 * (M1 * (M1 ~)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M3 * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K

K181(n, the U1 of K) is M8( the U1 of K)

0. K is V55(K) M2( the U1 of K)

K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))

K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))

K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K

M2 * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * (M1 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * (M1 * (M1 ~)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 * M1) * (M1 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K

K181(n, the U1 of K) is M8( the U1 of K)

0. K is V55(K) M2( the U1 of K)

K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))

K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))

K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K

M2 * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * (M1 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * (M1 * (M1 ~)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 * M1) * (M1 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

width (M2 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

(M1 * M2) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 * M1) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 * M1) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M2 * M1) * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * (M1 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 * (M1 * M1)) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K

K181(n, the U1 of K) is M8( the U1 of K)

0. K is V55(K) M2( the U1 of K)

K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))

K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))

K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))

M2 * (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 * (0. (K,n))) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(0. (K,n,n)) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K

K181(n, the U1 of K) is M8( the U1 of K)

0. K is V55(K) M2( the U1 of K)

K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))

K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))

K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 + M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 + M2) * (M1 + M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M1) + (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) + (0. (K,n))) + (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(((M1 * M1) + (0. (K,n))) + (0. (K,n))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) + (0. (K,n))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(0. (K,n)) + (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

- (M2 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 + M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K

K181(n, the U1 of K) is M8( the U1 of K)

0. K is V55(K) M2( the U1 of K)

K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))

K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))

K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))

M2 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

len (M1 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (M1 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

(M1 * M1) + (M2 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

len ((M1 * M1) + (M2 * M1)) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width ((M1 * M1) + (M2 * M1)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len (M2 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (M2 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len (M1 * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (M1 * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len (M1 + M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width (M1 + M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

(M1 + M2) * (M1 + M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 + M2) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 + M2) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 + M2) * M1) + ((M1 + M2) * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) + (M2 * M1)) + ((M1 + M2) * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M2) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) + (M2 * M1)) + ((M1 * M2) + (M2 * M2)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) + (M2 * M1)) + (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(((M1 * M1) + (M2 * M1)) + (M1 * M2)) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M2 * M1) + (- (M2 * M1)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M1) + ((M2 * M1) + (- (M2 * M1))) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) + ((M2 * M1) + (- (M2 * M1)))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M1) + (0. (K,n,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

((M1 * M1) + (0. (K,n,n))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(0. (K,n)) + (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

(M1 @) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K

K181(n, the U1 of K) is M8( the U1 of K)

0. K is V55(K) M2( the U1 of K)

K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))

K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))

K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))

(0. (K,n)) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(n,n) --> (0. K) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

K179(n,(0. K)) is V1() Function-like FinSequence-like set

K179(n,K179(n,(0. K))) is V1() Function-like FinSequence-like set

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K

K181(n, the U1 of K) is M8( the U1 of K)

0. K is V55(K) M2( the U1 of K)

K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))

K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))

K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

K181(n, the U1 of K) is M8( the U1 of K)

0. K is V55(K) M2( the U1 of K)

K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))

K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))

K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K

Indices (1. (K,n)) is set

dom (1. (K,n)) is M2( bool K97())

width (1. (K,n)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

Seg (width (1. (K,n))) is M2( bool K97())

{ b

[:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] is set

Seg n is M2( bool K97())

{ b

[:(Seg n),(Seg n):] is set

0 + 1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

[1,1] is set

Indices (0. (K,n)) is set

dom (0. (K,n)) is M2( bool K97())

width (0. (K,n)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

Seg (width (0. (K,n))) is M2( bool K97())

{ b

[:(dom (0. (K,n))),(Seg (width (0. (K,n)))):] is set

(0. (K,n)) * (1,1) is M2( the U1 of K)

1. K is V55(K) M2( the U1 of K)

n is V24() V25() V26() V30() V31() V32() ext-real V113() set

K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()

the U1 of K is V11() non trivial set

K180( the U1 of K) is M8( the U1 of K)

M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())

len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())

1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K

M1 * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

(M1 * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K

K181(n, the U1 of K) is M8( the U1 of K)

0. K is V55(K) M2( the U1 of K)

K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))

K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))

K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))

(0. (K,n)) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K

n is V24() V25() V26() V30() V31() V32