:: MATRIX_6 semantic presentation

K97() is V14() V24() V25() V26() M2( bool K93())
K93() is set
bool K93() is set
K92() is V14() V24() V25() V26() set
bool K92() is set
bool K97() is set
1 is set
2 is set
0 is set
0 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
n is ext-real V24() V25() V26() V30() V105() set
M3 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M3 * M3 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
M3 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M5 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M3 * M5 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
M5 * M3 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
n is ext-real V24() V25() V26() V30() V105() set
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M3 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M5 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M3 * M5 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
M5 * M3 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
n is ext-real V24() V25() V26() V30() V105() set
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
- M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len (- M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
width (- M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
n is ext-real V24() V25() V26() V30() V105() set
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 + M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len (M1 + M2) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (M1 + M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
n is ext-real V24() V25() V26() V30() V105() set
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 - M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
- M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
M1 + (- M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
(n,K,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len (n,K,M1,(n,K,M2)) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
M1 * M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len (M1 * M2) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (M1 * M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
n is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of n is V14() non trivial set
K147( the U1 of n) is M8( the U1 of n)
K is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
len K is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
0. (n,(len K),(len K)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of len K, len K, the U1 of n
(0. (n,(len K),(len K))) * K is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
width K is ext-real V24() V25() V26() V30() V105() M2(K97())
0. (n,(len K),(width K)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of len K, width K, the U1 of n
- ((0. (n,(len K),(len K))) * K) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
width (- ((0. (n,(len K),(len K))) * K)) is ext-real V24() V25() V26() V30() V105() M2(K97())
width ((0. (n,(len K),(len K))) * K) is ext-real V24() V25() V26() V30() V105() M2(K97())
len (0. (n,(len K),(len K))) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (0. (n,(len K),(len K))) is ext-real V24() V25() V26() V30() V105() M2(K97())
len ((0. (n,(len K),(len K))) * K) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
((len K),n,(0. (n,(len K),(len K))),(0. (n,(len K),(len K)))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of len K, len K, the U1 of n
((len K),n,(0. (n,(len K),(len K))),(0. (n,(len K),(len K)))) * K is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
((0. (n,(len K),(len K))) * K) + ((0. (n,(len K),(len K))) * K) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
len (- ((0. (n,(len K),(len K))) * K)) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(((0. (n,(len K),(len K))) * K) + ((0. (n,(len K),(len K))) * K)) + (- ((0. (n,(len K),(len K))) * K)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
((0. (n,(len K),(len K))) * K) - ((0. (n,(len K),(len K))) * K) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
((0. (n,(len K),(len K))) * K) + (- ((0. (n,(len K),(len K))) * K)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
((0. (n,(len K),(len K))) * K) + (((0. (n,(len K),(len K))) * K) - ((0. (n,(len K),(len K))) * K)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
len (0. (n,(len K),(len K))) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (0. (n,(len K),(len K))) is ext-real V24() V25() V26() V30() V105() M2(K97())
len ((0. (n,(len K),(len K))) * K) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len (0. (n,(len K),(width K))) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
n is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of n is V14() non trivial set
K147( the U1 of n) is M8( the U1 of n)
K is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
width K is ext-real V24() V25() V26() V30() V105() M2(K97())
0. (n,(width K),(width K)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of width K, width K, the U1 of n
K * (0. (n,(width K),(width K))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
len K is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
0. (n,(len K),(width K)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of len K, width K, the U1 of n
- (K * (0. (n,(width K),(width K)))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
width (- (K * (0. (n,(width K),(width K))))) is ext-real V24() V25() V26() V30() V105() M2(K97())
width (K * (0. (n,(width K),(width K)))) is ext-real V24() V25() V26() V30() V105() M2(K97())
len (0. (n,(width K),(width K))) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len (K * (0. (n,(width K),(width K)))) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (0. (n,(width K),(width K))) is ext-real V24() V25() V26() V30() V105() M2(K97())
((width K),n,(0. (n,(width K),(width K))),(0. (n,(width K),(width K)))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of width K, width K, the U1 of n
K * ((width K),n,(0. (n,(width K),(width K))),(0. (n,(width K),(width K)))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
(K * (0. (n,(width K),(width K)))) + (K * (0. (n,(width K),(width K)))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
len (- (K * (0. (n,(width K),(width K))))) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
((K * (0. (n,(width K),(width K)))) + (K * (0. (n,(width K),(width K))))) + (- (K * (0. (n,(width K),(width K))))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
(K * (0. (n,(width K),(width K)))) - (K * (0. (n,(width K),(width K)))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
(K * (0. (n,(width K),(width K)))) + (- (K * (0. (n,(width K),(width K))))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
(K * (0. (n,(width K),(width K)))) + ((K * (0. (n,(width K),(width K)))) - (K * (0. (n,(width K),(width K))))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
0. (K,n,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(0. (K,n,n)),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(0. (K,n,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len (0. (K,n,n)) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M3 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M3) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M3 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M3 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,(n,K,M2,M3),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M3,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M3,M2),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M3,(n,K,M2,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M3,(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M3,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M3,M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M3) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M3),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M3,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M2,M3)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M3 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M3) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M3 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M3 is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M2,M3),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M3,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M1),(n,K,M3,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(n,K,M3,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M3) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(n,K,M1,M3)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M2,M3)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(1. (K,n)),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M3 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M3 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M3,(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M3,(n,K,M2,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M3,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M3,M2),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(1. (K,n)),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
n is ext-real V24() V25() V26() V30() V105() set
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M3 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
(n,K,(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(1. (K,n)),(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
(n,K,(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(1. (K,n)))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
K147( the U1 of K) is M8( the U1 of K)
(1. (K,n)) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len (1. (K,n)) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
Indices (1. (K,n)) is set
Seg n is M2( bool K97())
[:(Seg n),(Seg n):] is set
M1 is ext-real V24() V25() V26() V30() V105() set
M2 is ext-real V24() V25() V26() V30() V105() set
[M1,M2] is set
(1. (K,n)) * (M1,M2) is M2( the U1 of K)
((1. (K,n)) @) * (M1,M2) is M2( the U1 of K)
[M2,M1] is set
0. K is V50(K) M2( the U1 of K)
(1. (K,n)) * (M2,M1) is M2( the U1 of K)
width (1. (K,n)) is ext-real V24() V25() V26() V30() V105() M2(K97())
len ((1. (K,n)) @) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width ((1. (K,n)) @) is ext-real V24() V25() V26() V30() V105() M2(K97())
n is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of n is V14() non trivial set
K is ext-real V24() V25() V26() V30() V105() set
1. (n,K) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
K147( the U1 of n) is M8( the U1 of n)
(1. (n,K)) @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,((1. (n,K)) @)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M2 @),(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,(M1 @),(M2 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
width (n,K,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,(n,K,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M1) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M1 @),((n,K,M1) @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len (n,K,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,M1,(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M1)) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,((n,K,M1) @),(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of n is V14() non trivial set
K147( the U1 of n) is M8( the U1 of n)
K is ext-real V24() V25() V26() V30() V105() set
M1 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M2 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M2,M1) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M3 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M5 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M3,M5) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M3 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M3 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M5 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (K,n,M2,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
(K,n,(K,n,M2,M1),(K,n,M3,M5)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M2,M1),M3) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,(K,n,M2,M1),M3),M5) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1,M3) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M2,(K,n,M1,M3)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M2,(K,n,M1,M3)),M5) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
1. (n,K) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M2,(1. (n,K))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M2,(1. (n,K))),M5) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M2,M5) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
width M5 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (K,n,M3,M5) is ext-real V24() V25() V26() V30() V105() M2(K97())
(K,n,(K,n,M3,M5),(K,n,M2,M1)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M3,M5),M2) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,(K,n,M3,M5),M2),M1) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M5,M2) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M3,(K,n,M5,M2)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M3,(K,n,M5,M2)),M1) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M3,(1. (n,K))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M3,(1. (n,K))),M1) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M3,M1) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
n is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of n is V14() non trivial set
K147( the U1 of n) is M8( the U1 of n)
K is ext-real V24() V25() V26() V30() V105() set
M1 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M2 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M2,M1) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1,M2) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
0. (K,n,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(1. (K,n)),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(0. (K,n,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(1. (K,n)),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M1,(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
n is ext-real V24() V25() V26() V30() V105() set
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
(1. (K,n)) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
M1 is M2( the U1 of K)
(n,n) --> M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
K147( the U1 of K) is M8( the U1 of K)
((n,n) --> M1) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len ((n,n) --> M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len (((n,n) --> M1) @) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
Indices ((n,n) --> M1) is set
Seg n is M2( bool K97())
[:(Seg n),(Seg n):] is set
Indices (((n,n) --> M1) @) is set
M2 is ext-real V24() V25() V26() V30() V105() set
M3 is ext-real V24() V25() V26() V30() V105() set
[M2,M3] is set
(((n,n) --> M1) @) * (M2,M3) is M2( the U1 of K)
((n,n) --> M1) * (M2,M3) is M2( the U1 of K)
[M3,M2] is set
((n,n) --> M1) * (M3,M2) is M2( the U1 of K)
width ((n,n) --> M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
width (((n,n) --> M1) @) is ext-real V24() V25() V26() V30() V105() M2(K97())
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
M1 is M2( the U1 of K)
(n,n) --> M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
K147( the U1 of K) is M8( the U1 of K)
((n,n) --> M1) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M1 @),(M2 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
Indices ((n,K,M1,M2) @) is set
M3 is ext-real V24() V25() V26() V30() V105() set
M5 is ext-real V24() V25() V26() V30() V105() set
[M3,M5] is set
((n,K,M1,M2) @) * (M3,M5) is M2( the U1 of K)
(n,K,(M1 @),(M2 @)) * (M3,M5) is M2( the U1 of K)
Seg n is M2( bool K97())
[:(Seg n),(Seg n):] is set
Indices (M1 @) is set
[M5,M3] is set
Indices M1 is set
Indices M2 is set
Indices (n,K,M1,M2) is set
(n,K,M1,M2) * (M5,M3) is M2( the U1 of K)
M1 * (M5,M3) is M2( the U1 of K)
M2 * (M5,M3) is M2( the U1 of K)
(M1 * (M5,M3)) + (M2 * (M5,M3)) is M2( the U1 of K)
(M1 @) * (M3,M5) is M2( the U1 of K)
((M1 @) * (M3,M5)) + (M2 * (M5,M3)) is M2( the U1 of K)
(M2 @) * (M3,M5) is M2( the U1 of K)
((M1 @) * (M3,M5)) + ((M2 @) * (M3,M5)) is M2( the U1 of K)
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M1 @),(M2 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(M2 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
Indices M1 is set
Seg n is M2( bool K97())
[:(Seg n),(Seg n):] is set
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is ext-real V24() V25() V26() V30() V105() set
M3 is ext-real V24() V25() V26() V30() V105() set
[M2,M3] is set
(M1 @) * (M2,M3) is M2( the U1 of K)
M1 * (M2,M3) is M2( the U1 of K)
[M3,M2] is set
0. K is V50(K) M2( the U1 of K)
M1 * (M3,M2) is M2( the U1 of K)
0. K is V50(K) M2( the U1 of K)
M1 * (M3,M2) is M2( the U1 of K)
n is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of n is V14() non trivial set
K147( the U1 of n) is M8( the U1 of n)
K is ext-real V24() V25() V26() V30() V105() set
M1 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1) @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M1 @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(M1 @)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
Indices ((K,n,M1) @) is set
M2 is ext-real V24() V25() V26() V30() V105() set
M3 is ext-real V24() V25() V26() V30() V105() set
[M2,M3] is set
((K,n,M1) @) * (M2,M3) is M2( the U1 of n)
(K,n,(M1 @)) * (M2,M3) is M2( the U1 of n)
Indices (M1 @) is set
Seg K is M2( bool K97())
[:(Seg K),(Seg K):] is set
[M3,M2] is set
Indices M1 is set
Indices (K,n,M1) is set
(K,n,M1) * (M3,M2) is M2( the U1 of n)
M1 * (M3,M2) is M2( the U1 of n)
- (M1 * (M3,M2)) is M2( the U1 of n)
(M1 @) * (M2,M3) is M2( the U1 of n)
- ((M1 @) * (M2,M3)) is M2( the U1 of n)
n is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of n is V14() non trivial set
K147( the U1 of n) is M8( the U1 of n)
K is ext-real V24() V25() V26() V30() V105() set
M1 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1) @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M1 @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(M1 @)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
n is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of n is V14() non trivial set
K147( the U1 of n) is M8( the U1 of n)
K is ext-real V24() V25() V26() V30() V105() set
M1 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M2 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1,M2) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
- M2 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
M1 + (- M2) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
(K,n,M1,M2) @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M1 @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M2) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M2) @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(M1 @),((K,n,M2) @)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1,((K,n,M2) @)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M2 @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(M2 @)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1,(K,n,(M2 @))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
n is ext-real V24() V25() V26() V30() V105() set
n is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital Fanoian L11()
the U1 of n is V14() non trivial set
K147( the U1 of n) is M8( the U1 of n)
K is ext-real V24() V25() V26() V30() V105() set
0. (n,K,K) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M1 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M1 @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
Indices M1 is set
M2 is ext-real V24() V25() V26() V30() V105() set
M3 is ext-real V24() V25() V26() V30() V105() set
[M2,M3] is set
M1 * (M2,M3) is M2( the U1 of n)
(0. (n,K,K)) * (M2,M3) is M2( the U1 of n)
- (M1 * (M2,M3)) is M2( the U1 of n)
(M1 * (M2,M3)) + (M1 * (M2,M3)) is M2( the U1 of n)
0. n is V50(n) M2( the U1 of n)
1_ n is M2( the U1 of n)
1. n is V50(n) M2( the U1 of n)
(1_ n) * (M1 * (M2,M3)) is M2( the U1 of n)
((1_ n) * (M1 * (M2,M3))) + (M1 * (M2,M3)) is M2( the U1 of n)
((1_ n) * (M1 * (M2,M3))) + ((1_ n) * (M1 * (M2,M3))) is M2( the U1 of n)
(1_ n) + (1_ n) is M2( the U1 of n)
((1_ n) + (1_ n)) * (M1 * (M2,M3)) is M2( the U1 of n)
Indices (0. (n,K,K)) is set
n is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital Fanoian L11()
the U1 of n is V14() non trivial set
K147( the U1 of n) is M8( the U1 of n)
0. n is V50(n) M2( the U1 of n)
K is ext-real V24() V25() V26() V30() V105() set
Seg K is M2( bool K97())
M1 is ext-real V24() V25() V26() V30() V105() set
M2 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M2 * (M1,M1) is M2( the U1 of n)
M2 @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M2) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
Indices M2 is set
[:(Seg K),(Seg K):] is set
[M1,M1] is set
(M2 @) * (M1,M1) is M2( the U1 of n)
- (M2 * (M1,M1)) is M2( the U1 of n)
(M2 * (M1,M1)) + (M2 * (M1,M1)) is M2( the U1 of n)
1_ n is M2( the U1 of n)
1. n is V50(n) M2( the U1 of n)
(1_ n) * (M2 * (M1,M1)) is M2( the U1 of n)
((1_ n) * (M2 * (M1,M1))) + (M2 * (M1,M1)) is M2( the U1 of n)
((1_ n) * (M2 * (M1,M1))) + ((1_ n) * (M2 * (M1,M1))) is M2( the U1 of n)
(1_ n) + (1_ n) is M2( the U1 of n)
((1_ n) + (1_ n)) * (M2 * (M1,M1)) is M2( the U1 of n)
n is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of n is V14() non trivial set
K147( the U1 of n) is M8( the U1 of n)
K is ext-real V24() V25() V26() V30() V105() set
M1 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M2 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1,M2) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
(K,n,M1,M2) @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M1 @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M2 @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(M1 @),(M2 @)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M1),(M2 @)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M2) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M1),(K,n,M2)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
n is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of n is V14() non trivial set
K147( the U1 of n) is M8( the U1 of n)
K is ext-real V24() V25() V26() V30() V105() set
M1 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1) @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M1 @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(M1 @)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M1)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
n is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of n is V14() non trivial set
K147( the U1 of n) is M8( the U1 of n)
K is ext-real V24() V25() V26() V30() V105() set
M1 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M2 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1,M2) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
- M2 is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
M1 + (- M2) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular FinSequence of K147( the U1 of n)
(K,n,M2) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
len (K,n,M2) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (K,n,M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
(K,n,M1,M2) @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M1 @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M2) @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(M1 @),((K,n,M2) @)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,M1) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M1),((K,n,M2) @)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
M2 @ is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(M2 @)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M1),(K,n,(M2 @))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M2)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M1),(K,n,(K,n,M2))) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
(K,n,(K,n,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of n)) V9() FinSequence-like tabular Matrix of K,K, the U1 of n
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
- (M1 @) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
M1 + (- (M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len (M1 @) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (M1 @) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,M1,(M1 @)) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M1 @)) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M1 @),((n,K,(M1 @)) @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 @) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,((M1 @) @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M1 @),(n,K,((M1 @) @))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M1 @),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
- M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
(M1 @) + (- M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular FinSequence of K147( the U1 of K)
(n,K,(n,K,M1,(M1 @))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M1),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M1),(n,K,M1,M2)),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,M1,M1),(n,K,M1,M2)),(n,K,M1,M2)),(n,K,M2,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len (n,K,M1,M2) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1,M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,(n,K,M1,M1),(n,K,M1,M2)) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,(n,K,M1,M1),(n,K,M1,M2)) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M1,M2),(n,K,M2,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len (n,K,(n,K,M1,M2),(n,K,M2,M2)) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,(n,K,M1,M2),(n,K,M2,M2)) is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M1,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M1),(n,K,M2,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len (n,K,(n,K,M1,M1),(n,K,M2,M1)) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,(n,K,M1,M1),(n,K,M2,M1)) is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M1,M2) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1,M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M1,M2),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),M1),(n,K,(n,K,M1,M2),M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M1),(n,K,M2,M1)),(n,K,(n,K,M1,M2),M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M1),(n,K,M2,M1)),(n,K,(n,K,M1,M2),(n,K,M2,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M1),(n,K,M2,M1)),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,M1,M1),(n,K,M2,M1)),(n,K,M1,M2)),(n,K,M2,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len (n,K,M2,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M2,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M1,M2),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),M1),(n,K,(n,K,M1,M2),M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M1),(n,K,M2,M1)),(n,K,(n,K,M1,M2),M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M1),(n,K,M2,M1)),(n,K,(n,K,M1,M2),(n,K,M2,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M1),(n,K,M2,M1)),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,M1,M1),(n,K,M2,M1)),(n,K,M1,M2)),(n,K,M2,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M1),(n,K,M1,M2)),(n,K,(n,K,M1,M2),(n,K,M2,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M1),(n,K,M1,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(n,K,M1,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len (n,K,M2) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1,M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M1,M2),(n,K,(n,K,M2),(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),(n,K,M2)),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M2,(n,K,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,(n,K,M2,(n,K,M2))),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular (n,K) Matrix of n,n, the U1 of K
(n,K,M1,(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,(1. (K,n))),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width (n,K,(n,K,M2),(n,K,M1)) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,(n,K,M2),(n,K,M1)),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M2),(n,K,M1)),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,M2),(n,K,M1)),M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2),(n,K,(n,K,M1),M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M2),(n,K,(n,K,M1),M1)),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2),(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M2),(1. (K,n))),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width (n,K,(n,K,M1),(n,K,M2)) is ext-real V24() V25() V26() V30() V105() M2(K97())
width (n,K,M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M2) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len (n,K,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1,M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M1,M2),(n,K,(n,K,M1),(n,K,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),(n,K,M1)),(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M1),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M2,M1),(n,K,M1)),(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M1,(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,(n,K,M1,(n,K,M1))),(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular (n,K) Matrix of n,n, the U1 of K
(n,K,M2,(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,(1. (K,n))),(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),(n,K,M2)),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),(n,K,M2)),(n,K,M2,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),(n,K,M2)),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,M1),(n,K,M2)),M2),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(n,K,(n,K,M2),M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),(n,K,(n,K,M2),M2)),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),(1. (K,n))),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular (n,K) Matrix of n,n, the U1 of K
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width (n,K,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M1),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(1. (K,n)),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular (n,K) Matrix of n,n, the U1 of K
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width (n,K,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M1),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(1. (K,n)),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len (n,K,M2,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M2,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular (n,K) Matrix of n,n, the U1 of K
(n,K,(1. (K,n)),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(n,K,M2,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M1),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(n,K,(n,K,M2,M1),(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M1,(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(n,K,M2,(n,K,M1,(n,K,M1)))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(n,K,M2,(1. (K,n)))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
n is ext-real V24() V25() V26() V30() V105() set
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular (n,K) Matrix of n,n, the U1 of K
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len (M1 @) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width (n,K,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,M1,(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(n,K,M1,(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(n,K,M1,(M1 @))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),M1),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),M1),(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(1. (K,n)),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(1. (K,n)),(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular (n,K) Matrix of n,n, the U1 of K
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M1 @),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (M1 @) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len (n,K,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),M1),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(M1 @),M1),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(n,K,M1,(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M1 @),(n,K,M1,(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M1 @),(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M1 @),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular (n,K) Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M2) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,(n,K,M2),(n,K,M1)) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,(n,K,M2),(n,K,M1)),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M2),(n,K,M1)),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,M2),(n,K,M1)),M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2),(n,K,(n,K,M1),M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M2),(n,K,(n,K,M1),M1)),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular (n,K) Matrix of n,n, the U1 of K
(n,K,(n,K,M2),(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M2),(1. (K,n))),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width (n,K,M1,M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M1,M2),(n,K,(n,K,M2),(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),(n,K,M2)),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M2,(n,K,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,(n,K,M2,(n,K,M2))),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,(1. (K,n))),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,(n,K,M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width (n,K,(n,K,M1),M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,M2,(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular (n,K) Matrix of n,n, the U1 of K
(n,K,(1. (K,n)),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(1. (K,n)),M2),(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,M1),M1),M2),(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),(n,K,M1,M2)),(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),(n,K,M2,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),(n,K,M2,M1)),(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),(n,K,M2,M1)),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),M2),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,M1),M2),M1),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),M2),(n,K,M1,(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),M2),(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M1 @),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,(n,K,M1,M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M1),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M1),(n,K,M2,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M1,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,(n,K,M1,M2),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(n,K,M2,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M1),(n,K,M2,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len (n,K,M1,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M1,M1),(n,K,M2,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M1),M2),(n,K,(n,K,M1,M1),M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),(n,K,M1,M2)),(n,K,(n,K,M1,M1),M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),(n,K,M1,M2)),(n,K,(n,K,M1,M2),(n,K,M1,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M1),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M2,M1),(n,K,M1,M2)),(n,K,(n,K,M1,M2),(n,K,M1,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M1),(n,K,M2,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M2,M1),(n,K,M2,M1)),(n,K,(n,K,M1,M2),(n,K,M1,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M2,M1),(n,K,M2,M1)),(n,K,(n,K,M2,M1),(n,K,M1,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M2,M1),(n,K,M2,M1)),(n,K,(n,K,M2,M1),(n,K,M2,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M1,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,(n,K,M1,M1)),(n,K,(n,K,M2,M1),(n,K,M2,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,(n,K,M1,M1)),(n,K,M2,(n,K,M1,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M2),(n,K,M1,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M1,M2) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1,M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M1,M2),(n,K,M2,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),M2),(n,K,(n,K,M1,M2),M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(n,K,M2,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),(n,K,M2,M2)),(n,K,(n,K,M1,M2),M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),(n,K,M2,M2)),(n,K,(n,K,M1,M2),(n,K,M2,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M1),(n,K,M2,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M2,M1),(n,K,M2,M2)),(n,K,(n,K,M1,M2),(n,K,M2,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M2,M1),(n,K,M2,M2)),(n,K,(n,K,M2,M1),(n,K,M2,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,(n,K,M1,M2)),(n,K,(n,K,M2,M1),(n,K,M2,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,(n,K,M1,M2)),(n,K,M2,(n,K,M1,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M2),(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,(n,K,M1,M2),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,(n,K,M1,M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M2,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M1,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M1,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M1,M1),(n,K,M2,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M1),M2),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M1,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,(n,K,M1,M2)),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M2,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,(n,K,M2,M1)),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M2,M1),M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M1,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,(n,K,M1,M1)),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,(n,K,M1,M1),M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M1,(n,K,M1,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M1,(n,K,M2,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,(n,K,M1,M2),M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,(n,K,M2,M1),M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M2,(n,K,M1,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2,M2),(n,K,M1,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,(M1 @),(M2 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,M1) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M2 @),(M1 @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M3 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),M3) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),M3)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M3) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M3),(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M3),(n,K,M2)),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len M3 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
width M3 is ext-real V24() V25() V26() V30() V105() M2(K97())
width (n,K,M1,M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,M2,M3) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len (n,K,M2,M3) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,(n,K,(n,K,M3),(n,K,M2)),(n,K,M1)) is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,(n,K,M1,M2),M3) is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M2),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len (n,K,(n,K,M2),(n,K,M1)) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len (n,K,M3) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,(n,K,M3),(n,K,M2)) is ext-real V24() V25() V26() V30() V105() M2(K97())
width (n,K,M3) is ext-real V24() V25() V26() V30() V105() M2(K97())
width (n,K,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len (n,K,M2) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,(n,K,(n,K,M3),(n,K,M2)),(n,K,M1)),(n,K,(n,K,M1,M2),M3)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M2,M3)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,M3),(n,K,M2)),(n,K,M1)),(n,K,M1,(n,K,M2,M3))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,M3),(n,K,M2)),(n,K,M1)),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,(n,K,M3),(n,K,M2)),(n,K,M1)),M1),(n,K,M2,M3)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M3),(n,K,M2)),(n,K,(n,K,M1),M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,M3),(n,K,M2)),(n,K,(n,K,M1),M1)),(n,K,M2,M3)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular (n,K) Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M3),(n,K,M2)),(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,M3),(n,K,M2)),(1. (K,n))),(n,K,M2,M3)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M3),(n,K,M2)),(n,K,M2,M3)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M3),(n,K,M2)),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,M3),(n,K,M2)),M2),M3) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M3),(n,K,(n,K,M2),M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M3),(n,K,(n,K,M2),M2)),M3) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M3),(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M3),(1. (K,n))),M3) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M3),M3) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),M3),(n,K,(n,K,(n,K,M3),(n,K,M2)),(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M3),(n,K,(n,K,M2),(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),M3),(n,K,(n,K,M3),(n,K,(n,K,M2),(n,K,M1)))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),M3),(n,K,M3)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,(n,K,M1,M2),M3),(n,K,M3)),(n,K,(n,K,M2),(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M3,(n,K,M3)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(n,K,M3,(n,K,M3))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),(n,K,M3,(n,K,M3))),(n,K,(n,K,M2),(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),(1. (K,n))),(n,K,(n,K,M2),(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(n,K,(n,K,M2),(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1,M2),(n,K,M2)),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2,(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M2,(n,K,M2))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,(n,K,M2,(n,K,M2))),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,(1. (K,n))),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M3 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1,M2),M3) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M3) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M3),(n,K,M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M3),(n,K,M2)),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
(n,K,(n,K,(n,K,M1,M2),M3)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
M3 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width (n,K,M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
width (n,K,M3) is ext-real V24() V25() V26() V30() V105() M2(K97())
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
width (n,K,M1,M2) is ext-real V24() V25() V26() V30() V105() M2(K97())
len (n,K,M1) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len (n,K,M2) is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
len M3 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width M3 is ext-real V24() V25() V26() V30() V105() M2(K97())
(n,K,(n,K,M1,M2),M3) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1,M2) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(M3 @),((n,K,M1,M2) @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2),(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M3),(n,K,(n,K,M2),(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
1. (K,n) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular (n,K) Matrix of n,n, the U1 of K
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
(1. (K,n)) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(1. (K,n))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
n is ext-real V24() V25() V26() V30() V105() set
K is V43() V47() non trivial V69() almost_left_invertible unital V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the U1 of K is V14() non trivial set
K147( the U1 of K) is M8( the U1 of K)
M1 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,(n,K,M1),M2)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,M2) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2),(n,K,(n,K,M1))) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2),M1) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
len M2 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
width (n,K,M1) is ext-real V24() V25() V26() V30() V105() M2(K97())
width M2 is ext-real V24() V25() V26() V30() V105() M2(K97())
width M1 is ext-real V24() V25() V26() V30() V105() M2(K97())
len M1 is ext-real V24() V25() V26() V30() V105() M3(K93(),K97())
M1 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
M2 @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M1),M2) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 @) @ is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K
(n,K,(n,K,M2),((M1 @) @)) is V4() V7(K97()) V8(K147( the U1 of K)) V9() FinSequence-like tabular Matrix of n,n, the U1 of K