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