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())
{ b1 where b1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97()) : ( 1 <= b1 & b1 <= width (1. (K,n)) ) } is set
[:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] is set
Seg n is M2( bool K97())
{ b1 where b1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97()) : ( 1 <= b1 & b1 <= n ) } is set
[:(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())
{ b1 where b1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97()) : ( 1 <= b1 & b1 <= width (0. (K,n)) ) } is set
[:(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() 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
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 * 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()
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
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 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
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 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
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
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) 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)) ~ 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
(((1. (K,n)) ~) * 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
(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
((1. (K,n)) * 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
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
M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M5 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M5 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M5 ~) * c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M5 ~) * c6) * M5 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M5 ~) ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M5 ~) ~) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M5 ~) ~) * M3) * (M5 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width c6 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M5 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
len c6 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M5 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width M5 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len ((M5 ~) * c6) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width ((M5 ~) * c6) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M5 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
M5 * (((M5 ~) * c6) * M5) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M5 * (((M5 ~) * c6) * M5)) * (M5 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M5 * ((M5 ~) * c6) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M5 * ((M5 ~) * c6)) * M5 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M5 * ((M5 ~) * c6)) * M5) * (M5 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M5 * (M5 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M5 * (M5 ~)) * c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M5 * (M5 ~)) * c6) * M5 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M5 * (M5 ~)) * c6) * M5) * (M5 ~) 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
(1. (K,n)) * c6 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)) * c6) * M5 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)) * c6) * M5) * (M5 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
c6 * M5 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(c6 * M5) * (M5 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
c6 * (M5 * (M5 ~)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
c6 * (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)
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
M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
c6 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(c6 ~) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((c6 ~) * M2) * c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M5 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M5 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M5 ~) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M5 ~) * M3) * M5 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M5 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
M5 * c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M5 * c6) ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M5 * c6) ~) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M5 * c6) ~) * M3) * (M5 * c6) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width ((M5 * c6) ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
M3 * M5 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len (M3 * M5) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M3 * M5) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len c6 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M5 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
len (M5 * c6) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (c6 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M5 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M5 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len ((M5 ~) * M3) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width ((M5 ~) * M3) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
(c6 ~) * ((M5 ~) * M3) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((c6 ~) * ((M5 ~) * M3)) * M5 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((c6 ~) * ((M5 ~) * M3)) * M5) * c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(c6 ~) * (M5 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((c6 ~) * (M5 ~)) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((c6 ~) * (M5 ~)) * M3) * M5 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((((c6 ~) * (M5 ~)) * M3) * M5) * c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M5 * c6) ~) * M3) * M5 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((((M5 * c6) ~) * M3) * M5) * c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M5 * c6) ~) * (M3 * M5) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M5 * c6) ~) * (M3 * M5)) * c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M3 * M5) * c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M5 * c6) ~) * ((M3 * M5) * c6) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M3 * (M5 * c6) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M5 * c6) ~) * (M3 * (M5 * c6)) 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
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 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M3 ~) * 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 ~) * M2) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width M3 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())
M2 * M3 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 * M3) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (((M3 ~) * M2) * M3) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M3 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width ((M3 ~) * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width (M3 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M3 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
(M3 ~) * (M2 * 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 ~) * M2) * M3) * ((M3 ~) * (M2 * 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 ~) * M2) * M3) * (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 ~) * M2) * M3) * (M3 ~)) * (M2 * 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 * (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 ~) * M2) * (M3 * (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 ~) * M2) * (M3 * (M3 ~))) * (M2 * 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) 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
((M3 ~) * 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
(((M3 ~) * M2) * (1. (K,n))) * (M2 * 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 ~) * M2) * (M2 * 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 ~) * 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
(((M3 ~) * M2) * M2) * M3 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
(M3 ~) * (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
((M3 ~) * (M2 * M2)) * 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
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 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M3 ~) * 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 ~) * M2) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width (M3 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width ((M3 ~) * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M3 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
M2 * M3 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 * M3) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (((M3 ~) * M2) * M3) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),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 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M3 ~) * (M2 * 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 ~) * M2) * M3) * ((M3 ~) * (M2 * 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 ~) * M2) * M3) * (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 ~) * M2) * M3) * (M3 ~)) * (M2 * 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 * (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 ~) * M2) * (M3 * (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 ~) * M2) * (M3 * (M3 ~))) * (M2 * 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) 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
((M3 ~) * 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
(((M3 ~) * M2) * (1. (K,n))) * (M2 * 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 ~) * M2) * (M2 * 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 ~) * 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
(((M3 ~) * M2) * M2) * M3 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
(M3 ~) * (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
((M3 ~) * (M2 * M2)) * M3 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))
(M3 ~) * (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
((M3 ~) * (0. (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
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)) * 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
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 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M3 ~) * 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 ~) * M2) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width ((M3 ~) * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width (M3 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
M2 * M3 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 * M3) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (((M3 ~) * M2) * M3) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M3 ~) 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 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 M3 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
(M3 ~) * (M2 * 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 ~) * M2) * M3) * ((M3 ~) * (M2 * 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 ~) * M2) * M3) * (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 ~) * M2) * M3) * (M3 ~)) * (M2 * 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 * (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 ~) * M2) * (M3 * (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 ~) * M2) * (M3 * (M3 ~))) * (M2 * 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) 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
((M3 ~) * 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
(((M3 ~) * M2) * (1. (K,n))) * (M2 * 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 ~) * M2) * (M2 * 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 ~) * 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
(((M3 ~) * M2) * M2) * M3 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
(M3 ~) * (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
((M3 ~) * (M2 * M2)) * 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 ~) * (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
((M3 ~) * (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
(M3 ~) * 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)
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
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 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
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 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M3 ~) * 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 ~) * M2) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len (1. (K,n)) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (1. (K,n)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width ((M3 ~) * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
len ((M3 ~) * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
(M3 ~) * (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
((M3 ~) * (M2 + (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
len (M3 ~) 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 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())
(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
((M3 ~) * M2) + ((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
(((M3 ~) * M2) + ((M3 ~) * (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
((M3 ~) * M2) + (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 ~) * M2) + (M3 ~)) * 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 ~) * 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 ~) * M2) * M3) + ((M3 ~) * 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
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
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 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M3 ~) * 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 ~) * M2) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width ((M3 ~) * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
(M3 ~) * (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
((M3 ~) * (M2 + M2)) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
len ((M3 ~) * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),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 (M3 ~) 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())
((M3 ~) * M2) + ((M3 ~) * 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 ~) * M2) + ((M3 ~) * M2)) * 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
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
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) + 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
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 ~) * 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 ~) * M2) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
len ((M3 ~) * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width ((M3 ~) * 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 (M3 ~) 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())
(M3 ~) * (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
((M3 ~) * (M2 + M2)) * 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 ~) * M2) + ((M3 ~) * 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 ~) * M2) + ((M3 ~) * M2)) * 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 ~) * ((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
((M3 ~) * ((M2 + M2) + M2)) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len ((M3 ~) * (M2 + M2)) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width ((M3 ~) * (M2 + M2)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M2 + M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M2 + M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
((M3 ~) * (M2 + M2)) + ((M3 ~) * 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 ~) * (M2 + M2)) + ((M3 ~) * M2)) * 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
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 M2 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
width (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
(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 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) * 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 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
(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
((1. (K,n)) * 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
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
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 ~ 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
((M3 ~) * 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
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
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 ~ 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
((M3 ~) * 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
(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
((M3 ~) * (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
width (M3 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M3 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 M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
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 * 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 * 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 * M3)) ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
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
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
c6 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 Matrix of n,n, the U1 of K
((1. (K,n)) @) * c6 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)) @) * c6) * (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
(1. (K,n)) * c6 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)) * c6) * (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
c6 * (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)
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
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 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M3 @) * 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 @) * M2) * 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 ~ 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
(((M3 ~) @) * 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
width (M3 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M3 @) 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())
width M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M3 ~) 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 ((M3 @) * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
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
M3 * (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 @) * M2) * (M3 * (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) 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
((M3 @) * 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
len M2 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())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
((M3 ~) @) * (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
((M3 ~) @) * (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 ~) @) * (M3 @)) * 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 * (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 * (M3 ~)) @) * 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 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
(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
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
M3 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())
c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
c6 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(c6 @) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((c6 @) * M2) * c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len c6 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
M5 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M5 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M5 @) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M5 @) * M3) * M5 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M5 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())
len (M5 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M5 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
M5 * c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M5 * c6) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M5 * c6) @) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M5 * c6) @) * M3) * (M5 * c6) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len ((M5 @) * M3) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
len (M5 * c6) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (c6 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width (M5 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width ((M5 @) * M3) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width c6 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
(c6 @) * (M5 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((c6 @) * (M5 @)) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((c6 @) * (M5 @)) * M3) * (M5 * c6) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(c6 @) * ((M5 @) * M3) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((c6 @) * ((M5 @) * M3)) * (M5 * c6) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M5 @) * M3) * (M5 * c6) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(c6 @) * (((M5 @) * M3) * (M5 * c6)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M5 @) * M3) * M5) * c6 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(c6 @) * ((((M5 @) * M3) * M5) * c6) 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
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
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 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M3 @) * 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 @) * M2) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width ((M3 @) * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
(M3 @) * (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
((M3 @) * (M2 + M2)) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
len ((M3 @) * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),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 (M3 @) 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())
((M3 @) * M2) + ((M3 @) * 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 @) * M2) + ((M3 @) * M2)) * 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
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
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) + 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
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 @) * 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 @) * M2) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
len ((M3 @) * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width ((M3 @) * 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 (M3 @) 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())
(M3 @) * (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
((M3 @) * (M2 + M2)) * 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 @) * M2) + ((M3 @) * 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 @) * M2) + ((M3 @) * M2)) * 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 @) * ((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
((M3 @) * ((M2 + M2) + M2)) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len ((M3 @) * (M2 + M2)) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width ((M3 @) * (M2 + M2)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M2 + M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M2 + M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
((M3 @) * (M2 + M2)) + ((M3 @) * 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 @) * (M2 + M2)) + ((M3 @) * M2)) * 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
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 M2 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
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
(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 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 * 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 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) * 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
(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
((1. (K,n)) * 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
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
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 @ 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
((M3 @) * 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
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 ~) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width (M3 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
(M3 ~) * 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 ~) * 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 @) * ((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) 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
len (M3 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
M3 * (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 * (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 ~) @) * (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
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
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 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M3 @) * 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 @) * M2) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width (M3 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
M2 * M3 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 * M3) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M2 * M3) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),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())
(M3 @) * (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 @) * (M2 @)) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M3 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())
(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 @) * (M2 @)) * ((M3 @) @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 * M3) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M2 * M3) @) * ((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 @) * (M2 * 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 @) * (M2 * 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
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) * 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 ~) * 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
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
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
diagonal_of_Matrix M1 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M1) is 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
(n,K,M1) is M2( the U1 of K)
diagonal_of_Matrix M1 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M1) is M2( 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,K,(M1 @)) is M2( the U1 of K)
diagonal_of_Matrix (M1 @) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (M1 @)) is M2( the U1 of K)
Seg n is M2( bool K97())
{ b1 where b1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97()) : ( 1 <= b1 & b1 <= n ) } is set
M2 is V24() V25() V26() V30() V31() V32() ext-real V113() set
(diagonal_of_Matrix M1) . M2 is set
(diagonal_of_Matrix (M1 @)) . M2 is set
M1 * (M2,M2) is M2( the U1 of K)
(M1 @) * (M2,M2) is M2( the U1 of K)
Indices M1 is set
dom M1 is M2( bool K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
Seg (width M1) is M2( bool K97())
{ b1 where b1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97()) : ( 1 <= b1 & b1 <= width M1 ) } is set
[:(dom M1),(Seg (width M1)):] is set
[:(Seg n),(Seg n):] is set
[M2,M2] is set
len (diagonal_of_Matrix (M1 @)) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
dom (diagonal_of_Matrix (M1 @)) is M2( bool K97())
len (diagonal_of_Matrix M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
dom (diagonal_of_Matrix M1) is M2( bool K97())
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
(n,K,M1) is M2( the U1 of K)
diagonal_of_Matrix M1 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M1) is M2( 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
(n,K,(M1 + M2)) is M2( the U1 of K)
diagonal_of_Matrix (M1 + M2) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (M1 + M2)) is M2( the U1 of K)
(n,K,M2) is M2( the U1 of K)
diagonal_of_Matrix M2 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M2) is M2( the U1 of K)
(n,K,M1) + (n,K,M2) is M2( the U1 of K)
the U5 of K is V1() V4([: the U1 of K, the U1 of K:]) V5( the U1 of K) Function-like V18([: the U1 of K, the U1 of K:], the U1 of K) M2( bool [:[: the U1 of K, the U1 of K:], the U1 of K:])
[: the U1 of K, the U1 of K:] is set
[:[: the U1 of K, the U1 of K:], the U1 of K:] is set
bool [:[: the U1 of K, the U1 of K:], the U1 of K:] is set
K84( the U1 of K, the U5 of K,(n,K,M1),(n,K,M2)) is M2( the U1 of K)
len (diagonal_of_Matrix M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
dom (diagonal_of_Matrix M1) is M2( bool K97())
Seg n is M2( bool K97())
{ b1 where b1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97()) : ( 1 <= b1 & b1 <= n ) } is set
len (diagonal_of_Matrix (M1 + M2)) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
dom (diagonal_of_Matrix (M1 + M2)) is M2( bool K97())
len (diagonal_of_Matrix M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
dom (diagonal_of_Matrix M2) is M2( bool K97())
(diagonal_of_Matrix M1) + (diagonal_of_Matrix M2) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
K221( the U1 of K, the U1 of K, the U1 of K, the U5 of K,(diagonal_of_Matrix M1),(diagonal_of_Matrix M2)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
dom ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) is M2( bool K97())
M3 is V24() V25() V26() V30() V31() V32() ext-real V113() set
((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . M3 is set
(diagonal_of_Matrix (M1 + M2)) . M3 is set
(M1 + M2) * (M3,M3) is M2( the U1 of K)
Indices M1 is set
dom M1 is M2( bool K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
Seg (width M1) is M2( bool K97())
{ b1 where b1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97()) : ( 1 <= b1 & b1 <= width M1 ) } is set
[:(dom M1),(Seg (width M1)):] is set
[:(Seg n),(Seg n):] is set
[M3,M3] is set
(diagonal_of_Matrix M1) . M3 is set
M1 * (M3,M3) is M2( the U1 of K)
(diagonal_of_Matrix M2) . M3 is set
M2 * (M3,M3) is M2( the U1 of K)
(M1 * (M3,M3)) + (M2 * (M3,M3)) is M2( the U1 of K)
K84( the U1 of K, the U5 of K,(M1 * (M3,M3)),(M2 * (M3,M3))) is M2( the U1 of K)
Sum ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) is M2( the U1 of K)
(Sum (diagonal_of_Matrix M1)) + (Sum (diagonal_of_Matrix M2)) is M2( the U1 of K)
K84( the U1 of K, the U5 of K,(Sum (diagonal_of_Matrix M1)),(Sum (diagonal_of_Matrix M2))) is 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
(n,K,M1) is M2( the U1 of K)
diagonal_of_Matrix M1 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M1) is M2( 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
(n,K,M2) is M2( the U1 of K)
diagonal_of_Matrix M2 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M2) is M2( the U1 of K)
(n,K,M1) + (n,K,M2) is M2( the U1 of K)
the U5 of K is V1() V4([: the U1 of K, the U1 of K:]) V5( the U1 of K) Function-like V18([: the U1 of K, the U1 of K:], the U1 of K) M2( bool [:[: the U1 of K, the U1 of K:], the U1 of K:])
[: the U1 of K, the U1 of K:] is set
[:[: the U1 of K, the U1 of K:], the U1 of K:] is set
bool [:[: the U1 of K, the U1 of K:], the U1 of K:] is set
K84( the U1 of K, the U5 of K,(n,K,M1),(n,K,M2)) is M2( 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 + M2) + 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,K,((M1 + M2) + M3)) is M2( the U1 of K)
diagonal_of_Matrix ((M1 + M2) + M3) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix ((M1 + M2) + M3)) is M2( the U1 of K)
(n,K,M3) is M2( the U1 of K)
diagonal_of_Matrix M3 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M3) is M2( the U1 of K)
((n,K,M1) + (n,K,M2)) + (n,K,M3) is M2( the U1 of K)
K84( the U1 of K, the U5 of K,((n,K,M1) + (n,K,M2)),(n,K,M3)) is M2( the U1 of K)
(n,K,(M1 + M2)) is M2( the U1 of K)
diagonal_of_Matrix (M1 + M2) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (M1 + M2)) is M2( the U1 of K)
(n,K,(M1 + M2)) + (n,K,M3) is M2( the U1 of K)
K84( the U1 of K, the U5 of K,(n,K,(M1 + M2)),(n,K,M3)) is 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()
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))
(n,K,(0. (K,n))) is M2( the U1 of K)
diagonal_of_Matrix (0. (K,n)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (0. (K,n))) is M2( the U1 of K)
len (diagonal_of_Matrix (0. (K,n))) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
dom (diagonal_of_Matrix (0. (K,n))) is M2( bool K97())
Seg n is M2( bool K97())
{ b1 where b1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97()) : ( 1 <= b1 & b1 <= n ) } is set
M1 is V24() V25() V26() V30() V31() V32() ext-real V113() set
(diagonal_of_Matrix (0. (K,n))) /. M1 is M2( the U1 of K)
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())
{ b1 where b1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97()) : ( 1 <= b1 & b1 <= width (0. (K,n)) ) } is set
[:(dom (0. (K,n))),(Seg (width (0. (K,n)))):] is set
[:(Seg n),(Seg n):] is set
[M1,M1] is set
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
Indices (0. (K,n,n)) is set
dom (0. (K,n,n)) is M2( bool K97())
width (0. (K,n,n)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
Seg (width (0. (K,n,n))) is M2( bool K97())
{ b1 where b1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97()) : ( 1 <= b1 & b1 <= width (0. (K,n,n)) ) } is set
[:(dom (0. (K,n,n))),(Seg (width (0. (K,n,n)))):] is set
(0. (K,n)) * (M1,M1) is M2( the U1 of K)
(diagonal_of_Matrix (0. (K,n))) . M1 is 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)
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
(n,K,(- M1)) is M2( the U1 of K)
diagonal_of_Matrix (- M1) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (- M1)) is M2( the U1 of K)
(n,K,M1) is M2( the U1 of K)
diagonal_of_Matrix M1 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M1) is M2( the U1 of K)
- (n,K,M1) is M2( 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())
(n,K,M1) + (n,K,(- M1)) is M2( the U1 of K)
the U5 of K is V1() V4([: the U1 of K, the U1 of K:]) V5( the U1 of K) Function-like V18([: the U1 of K, the U1 of K:], the U1 of K) M2( bool [:[: the U1 of K, the U1 of K:], the U1 of K:])
[: the U1 of K, the U1 of K:] is set
[:[: the U1 of K, the U1 of K:], the U1 of K:] is set
bool [:[: the U1 of K, the U1 of K:], the U1 of K:] is set
K84( the U1 of K, the U5 of K,(n,K,M1),(n,K,(- M1))) is M2( 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,K,(M1 + (- M1))) is M2( the U1 of K)
diagonal_of_Matrix (M1 + (- M1)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (M1 + (- M1))) is M2( 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))
(n,K,(0. (K,n,n))) is M2( the U1 of K)
diagonal_of_Matrix (0. (K,n,n)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (0. (K,n,n))) is M2( 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
(n,K,(0. (K,n))) is M2( the U1 of K)
diagonal_of_Matrix (0. (K,n)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (0. (K,n))) is 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
- 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,K,(- M1)) is M2( the U1 of K)
diagonal_of_Matrix (- M1) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (- M1)) is M2( the U1 of K)
- (n,K,(- M1)) is M2( the U1 of K)
(n,K,M1) is M2( the U1 of K)
diagonal_of_Matrix M1 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M1) is M2( 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())
(n,K,M1) + (n,K,(- M1)) is M2( the U1 of K)
the U5 of K is V1() V4([: the U1 of K, the U1 of K:]) V5( the U1 of K) Function-like V18([: the U1 of K, the U1 of K:], the U1 of K) M2( bool [:[: the U1 of K, the U1 of K:], the U1 of K:])
[: the U1 of K, the U1 of K:] is set
[:[: the U1 of K, the U1 of K:], the U1 of K:] is set
bool [:[: the U1 of K, the U1 of K:], the U1 of K:] is set
K84( the U1 of K, the U5 of K,(n,K,M1),(n,K,(- M1))) is M2( 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,K,(M1 + (- M1))) is M2( the U1 of K)
diagonal_of_Matrix (M1 + (- M1)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (M1 + (- M1))) is M2( 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))
(n,K,(0. (K,n,n))) is M2( the U1 of K)
diagonal_of_Matrix (0. (K,n,n)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (0. (K,n,n))) is M2( 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
(n,K,(0. (K,n))) is M2( the U1 of K)
diagonal_of_Matrix (0. (K,n)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (0. (K,n))) is 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)
0. K is V55(K) M2( 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
(n,K,(M1 + (- M1))) is M2( the U1 of K)
diagonal_of_Matrix (M1 + (- M1)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (M1 + (- M1))) is M2( 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())
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)
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,K,(0. (K,n,n))) is M2( the U1 of K)
diagonal_of_Matrix (0. (K,n,n)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (0. (K,n,n))) is M2( 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
(n,K,(0. (K,n))) is M2( the U1 of K)
diagonal_of_Matrix (0. (K,n)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (0. (K,n))) is 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
(n,K,M1) is M2( the U1 of K)
diagonal_of_Matrix M1 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M1) is M2( 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 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular FinSequence of K180( the U1 of K)
M1 + (- M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular FinSequence of K180( the U1 of K)
(n,K,(M1 - M2)) is M2( the U1 of K)
diagonal_of_Matrix (M1 - M2) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (M1 - M2)) is M2( the U1 of K)
(n,K,M2) is M2( the U1 of K)
diagonal_of_Matrix M2 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M2) is M2( the U1 of K)
(n,K,M1) - (n,K,M2) is M2( the U1 of K)
- (n,K,M2) is M2( the U1 of K)
K166(K,(n,K,M1),(- (n,K,M2))) is M2( the U1 of K)
the U5 of K is V1() V4([: the U1 of K, the U1 of K:]) V5( the U1 of K) Function-like V18([: the U1 of K, the U1 of K:], the U1 of K) M2( bool [:[: the U1 of K, the U1 of K:], the U1 of K:])
[: the U1 of K, the U1 of K:] is set
[:[: the U1 of K, the U1 of K:], the U1 of K:] is set
bool [:[: the U1 of K, the U1 of K:], the U1 of K:] is set
K84( the U1 of K, the U5 of K,(n,K,M1),(- (n,K,M2))) is M2( 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
(n,K,(- M2)) is M2( the U1 of K)
diagonal_of_Matrix (- M2) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (- M2)) is M2( the U1 of K)
(n,K,M1) + (n,K,(- M2)) is M2( the U1 of K)
K84( the U1 of K, the U5 of K,(n,K,M1),(n,K,(- M2))) is M2( the U1 of K)
(n,K,M1) + (- (n,K,M2)) is 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
(n,K,M1) is M2( the U1 of K)
diagonal_of_Matrix M1 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M1) is M2( 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 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular FinSequence of K180( the U1 of K)
M1 + (- M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular FinSequence of K180( the U1 of K)
(n,K,M2) is M2( the U1 of K)
diagonal_of_Matrix M2 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M2) is M2( the U1 of K)
(n,K,M1) - (n,K,M2) is M2( the U1 of K)
- (n,K,M2) is M2( the U1 of K)
K166(K,(n,K,M1),(- (n,K,M2))) is M2( the U1 of K)
the U5 of K is V1() V4([: the U1 of K, the U1 of K:]) V5( the U1 of K) Function-like V18([: the U1 of K, the U1 of K:], the U1 of K) M2( bool [:[: the U1 of K, the U1 of K:], the U1 of K:])
[: the U1 of K, the U1 of K:] is set
[:[: the U1 of K, the U1 of K:], the U1 of K:] is set
bool [:[: the U1 of K, the U1 of K:], the U1 of K:] is set
K84( the U1 of K, the U5 of K,(n,K,M1),(- (n,K,M2))) is M2( 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 - M2) + 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,K,((M1 - M2) + M3)) is M2( the U1 of K)
diagonal_of_Matrix ((M1 - M2) + M3) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix ((M1 - M2) + M3)) is M2( the U1 of K)
(n,K,M3) is M2( the U1 of K)
diagonal_of_Matrix M3 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M3) is M2( the U1 of K)
((n,K,M1) - (n,K,M2)) + (n,K,M3) is M2( the U1 of K)
K84( the U1 of K, the U5 of K,((n,K,M1) - (n,K,M2)),(n,K,M3)) is M2( the U1 of K)
(n,K,(M1 - M2)) is M2( the U1 of K)
diagonal_of_Matrix (M1 - M2) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (M1 - M2)) is M2( the U1 of K)
(n,K,(M1 - M2)) + (n,K,M3) is M2( the U1 of K)
K84( the U1 of K, the U5 of K,(n,K,(M1 - M2)),(n,K,M3)) is 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
(n,K,M1) is M2( the U1 of K)
diagonal_of_Matrix M1 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M1) is M2( 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
(n,K,M2) is M2( the U1 of K)
diagonal_of_Matrix M2 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M2) is M2( the U1 of K)
(n,K,M1) + (n,K,M2) is M2( the U1 of K)
the U5 of K is V1() V4([: the U1 of K, the U1 of K:]) V5( the U1 of K) Function-like V18([: the U1 of K, the U1 of K:], the U1 of K) M2( bool [:[: the U1 of K, the U1 of K:], the U1 of K:])
[: the U1 of K, the U1 of K:] is set
[:[: the U1 of K, the U1 of K:], the U1 of K:] is set
bool [:[: the U1 of K, the U1 of K:], the U1 of K:] is set
K84( the U1 of K, the U5 of K,(n,K,M1),(n,K,M2)) is M2( 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 + M2) - 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 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular FinSequence of K180( the U1 of K)
(M1 + M2) + (- M3) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular FinSequence of K180( the U1 of K)
(n,K,((M1 + M2) - M3)) is M2( the U1 of K)
diagonal_of_Matrix ((M1 + M2) - M3) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix ((M1 + M2) - M3)) is M2( the U1 of K)
(n,K,M3) is M2( the U1 of K)
diagonal_of_Matrix M3 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M3) is M2( the U1 of K)
((n,K,M1) + (n,K,M2)) - (n,K,M3) is M2( the U1 of K)
- (n,K,M3) is M2( the U1 of K)
K166(K,((n,K,M1) + (n,K,M2)),(- (n,K,M3))) is M2( the U1 of K)
K84( the U1 of K, the U5 of K,((n,K,M1) + (n,K,M2)),(- (n,K,M3))) is M2( the U1 of K)
(n,K,(M1 + M2)) is M2( the U1 of K)
diagonal_of_Matrix (M1 + M2) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (M1 + M2)) is M2( the U1 of K)
(n,K,(M1 + M2)) - (n,K,M3) is M2( the U1 of K)
K166(K,(n,K,(M1 + M2)),(- (n,K,M3))) is M2( the U1 of K)
K84( the U1 of K, the U5 of K,(n,K,(M1 + M2)),(- (n,K,M3))) is 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
(n,K,M1) is M2( the U1 of K)
diagonal_of_Matrix M1 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M1) is M2( 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 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular FinSequence of K180( the U1 of K)
M1 + (- M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular FinSequence of K180( the U1 of K)
(n,K,M2) is M2( the U1 of K)
diagonal_of_Matrix M2 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M2) is M2( the U1 of K)
(n,K,M1) - (n,K,M2) is M2( the U1 of K)
- (n,K,M2) is M2( the U1 of K)
K166(K,(n,K,M1),(- (n,K,M2))) is M2( the U1 of K)
the U5 of K is V1() V4([: the U1 of K, the U1 of K:]) V5( the U1 of K) Function-like V18([: the U1 of K, the U1 of K:], the U1 of K) M2( bool [:[: the U1 of K, the U1 of K:], the U1 of K:])
[: the U1 of K, the U1 of K:] is set
[:[: the U1 of K, the U1 of K:], the U1 of K:] is set
bool [:[: the U1 of K, the U1 of K:], the U1 of K:] is set
K84( the U1 of K, the U5 of K,(n,K,M1),(- (n,K,M2))) is M2( 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 - M2) - 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 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular FinSequence of K180( the U1 of K)
(M1 - M2) + (- M3) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular FinSequence of K180( the U1 of K)
(n,K,((M1 - M2) - M3)) is M2( the U1 of K)
diagonal_of_Matrix ((M1 - M2) - M3) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix ((M1 - M2) - M3)) is M2( the U1 of K)
(n,K,M3) is M2( the U1 of K)
diagonal_of_Matrix M3 is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix M3) is M2( the U1 of K)
((n,K,M1) - (n,K,M2)) - (n,K,M3) is M2( the U1 of K)
- (n,K,M3) is M2( the U1 of K)
K166(K,((n,K,M1) - (n,K,M2)),(- (n,K,M3))) is M2( the U1 of K)
K84( the U1 of K, the U5 of K,((n,K,M1) - (n,K,M2)),(- (n,K,M3))) is M2( the U1 of K)
(n,K,(M1 - M2)) is M2( the U1 of K)
diagonal_of_Matrix (M1 - M2) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like FinSequence of the U1 of K
Sum (diagonal_of_Matrix (M1 - M2)) is M2( the U1 of K)
(n,K,(M1 - M2)) - (n,K,M3) is M2( the U1 of K)
K166(K,(n,K,(M1 - M2)),(- (n,K,M3))) is M2( the U1 of K)
K84( the U1 of K, the U5 of K,(n,K,(M1 - M2)),(- (n,K,M3))) is M2( the U1 of K)