:: MATRIX12 semantic presentation

REAL is set
NAT is V11() V21() V22() V23() M2( bool REAL)
bool REAL is set
NAT is V11() V21() V22() V23() set
bool NAT is set
bool NAT is set
1 is V11() V21() V22() V23() V27() ext-real positive non negative M3( REAL , NAT )
2 is V11() V21() V22() V23() V27() ext-real positive non negative M3( REAL , NAT )
0 is V11() V21() V22() V23() V25() V26() V27() ext-real non positive non negative set
{0,1} is V11() set
0 is V11() V21() V22() V23() V25() V26() V27() ext-real non positive non negative M3( REAL , NAT )
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
Seg n is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= n ) } is set
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
a is V21() V22() V23() V27() ext-real non negative set
a is V21() V22() V23() V27() ext-real non negative set
A is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
width A is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width A) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width A ) } is set
Line (A,a) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of K
(width A) -tuples_on the carrier of K is functional V11() FinSequence-membered FinSequenceSet of the carrier of K
Line (A,a) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of K
M is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
M1 is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
M2 is V1() V4( NAT ) V5( the carrier of K) Function-like FinSequence-like FinSequence of the carrier of K
ReplaceLine (A,a,M2) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
i is V1() V4( NAT ) V5( the carrier of K) Function-like FinSequence-like FinSequence of the carrier of K
ReplaceLine (M,a,i) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
j is V21() V22() V23() V27() ext-real non negative set
p1 is V21() V22() V23() V27() ext-real non negative set
M1 * (j,p1) is M2( the carrier of K)
A * (a,p1) is M2( the carrier of K)
A * (a,p1) is M2( the carrier of K)
A * (j,p1) is M2( the carrier of K)
len M2 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
len i is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width M1 is V21() V22() V23() V27() ext-real non negative M2( NAT )
Line (M1,j) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width M1) FinSequence-like Element of (width M1) -tuples_on the carrier of K
(width M1) -tuples_on the carrier of K is functional V11() FinSequence-membered FinSequenceSet of the carrier of K
(Line (M1,j)) . p1 is set
i . p1 is set
len M2 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
Line (M1,j) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width M1) FinSequence-like Element of (width M1) -tuples_on the carrier of K
width M1 is V21() V22() V23() V27() ext-real non negative M2( NAT )
(width M1) -tuples_on the carrier of K is functional V11() FinSequence-membered FinSequenceSet of the carrier of K
Line (M,j) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width M) FinSequence-like Element of (width M) -tuples_on the carrier of K
(width M) -tuples_on the carrier of K is functional V11() FinSequence-membered FinSequenceSet of the carrier of K
len i is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
(Line (M1,j)) . p1 is set
M2 . p1 is set
Line (M,j) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width M) FinSequence-like Element of (width M) -tuples_on the carrier of K
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
(width M) -tuples_on the carrier of K is functional V11() FinSequence-membered FinSequenceSet of the carrier of K
Line (A,j) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of K
len M2 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len i is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width M1 is V21() V22() V23() V27() ext-real non negative M2( NAT )
Line (M1,j) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width M1) FinSequence-like Element of (width M1) -tuples_on the carrier of K
(width M1) -tuples_on the carrier of K is functional V11() FinSequence-membered FinSequenceSet of the carrier of K
(Line (M1,j)) . p1 is set
(Line (A,j)) . p1 is set
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
a is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len a is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom a is M2( bool NAT)
width a is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width a) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width a ) } is set
a is V21() V22() V23() V27() ext-real non negative set
A is V21() V22() V23() V27() ext-real non negative set
Line (a,a) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width a) FinSequence-like Element of (width a) -tuples_on the carrier of K
(width a) -tuples_on the carrier of K is functional V11() FinSequence-membered FinSequenceSet of the carrier of K
ReplaceLine (a,A,(Line (a,a))) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
Line (a,A) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width a) FinSequence-like Element of (width a) -tuples_on the carrier of K
ReplaceLine ((ReplaceLine (a,A,(Line (a,a)))),a,(Line (a,A))) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len (ReplaceLine ((ReplaceLine (a,A,(Line (a,a)))),a,(Line (a,A)))) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (Line (a,A)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg l is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= l ) } is set
len (Line (a,a)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (ReplaceLine (a,A,(Line (a,a)))) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (ReplaceLine (a,A,(Line (a,a)))) is V21() V22() V23() V27() ext-real non negative M2( NAT )
M2 is V21() V22() V23() V27() ext-real non negative set
i is V21() V22() V23() V27() ext-real non negative set
(ReplaceLine ((ReplaceLine (a,A,(Line (a,a)))),a,(Line (a,A)))) * (M2,i) is M2( the carrier of K)
a * (A,i) is M2( the carrier of K)
a * (a,i) is M2( the carrier of K)
a * (M2,i) is M2( the carrier of K)
M is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
M1 is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Indices M is set
dom M is M2( bool NAT)
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Indices a is set
[:(dom a),(Seg (width a)):] is set
M2 is V21() V22() V23() V27() ext-real non negative set
i is V21() V22() V23() V27() ext-real non negative set
[M2,i] is set
M * (M2,i) is M2( the carrier of K)
M1 * (M2,i) is M2( the carrier of K)
a * (a,i) is M2( the carrier of K)
a * (A,i) is M2( the carrier of K)
a * (M2,i) is M2( the carrier of K)
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
a is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
width a is V21() V22() V23() V27() ext-real non negative M2( NAT )
a is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
width a is V21() V22() V23() V27() ext-real non negative M2( NAT )
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of a is V11() non trivial set
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
A is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of a
dom A is M2( bool NAT)
(n,l,a,A,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of a
Line (A,a) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
width A is V21() V22() V23() V27() ext-real non negative M2( NAT )
(width A) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
Line (A,K) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
M is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of a
M1 is V21() V22() V23() V27() ext-real non negative set
Line (M,M1) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width M) FinSequence-like Element of (width M) -tuples_on the carrier of a
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
(width M) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
Line (A,M1) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
len (Line (M,M1)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
M2 is V21() V22() V23() V27() ext-real non negative set
Seg (width M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M ) } is set
(Line (M,M1)) . M2 is set
M * (M1,M2) is M2( the carrier of a)
A * (a,M2) is M2( the carrier of a)
(Line (A,a)) . M2 is set
len (Line (A,a)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (Line (M,M1)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
M2 is V21() V22() V23() V27() ext-real non negative set
Seg (width M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M ) } is set
(Line (M,M1)) . M2 is set
M * (M1,M2) is M2( the carrier of a)
A * (K,M2) is M2( the carrier of a)
(Line (A,K)) . M2 is set
len (Line (A,K)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (Line (M,M1)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
M2 is V21() V22() V23() V27() ext-real non negative set
Seg (width M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M ) } is set
(Line (M,M1)) . M2 is set
M * (M1,M2) is M2( the carrier of a)
A * (M1,M2) is M2( the carrier of a)
(Line (A,M1)) . M2 is set
len (Line (A,M1)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
a is M2( the carrier of K)
a is V21() V22() V23() V27() ext-real non negative set
A is V21() V22() V23() V27() ext-real non negative set
M is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
dom M is M2( bool NAT)
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M ) } is set
Line (M,a) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width M) FinSequence-like Element of (width M) -tuples_on the carrier of K
(width M) -tuples_on the carrier of K is functional V11() FinSequence-membered FinSequenceSet of the carrier of K
a * (Line (M,a)) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width M) FinSequence-like Element of (width M) -tuples_on the carrier of K
a multfield is V1() V4( the carrier of K) V5( the carrier of K) Function-like V18( the carrier of K, the carrier of K) M2( bool [: the carrier of K, the carrier of K:])
[: the carrier of K, the carrier of K:] is set
bool [: the carrier of K, the carrier of K:] is set
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
K38( the carrier of K) is V1() V4( the carrier of K) V5( the carrier of K) V11() V14( the carrier of K) M2( bool [: the carrier of K, the carrier of K:])
K162( the carrier of K, the carrier of K, the multF of K,a,K38( the carrier of K)) is V1() V4( the carrier of K) V5( the carrier of K) Function-like V18( the carrier of K, the carrier of K) M2( bool [: the carrier of K, the carrier of K:])
K174( the carrier of K, the carrier of K,(Line (M,a)),(a multfield)) is V1() V4( NAT ) V5( the carrier of K) Function-like FinSequence-like FinSequence of the carrier of K
(a * (Line (M,a))) . A is set
M * (a,A) is M2( the carrier of K)
a * (M * (a,A)) is M2( the carrier of K)
the multF of K . (a,(M * (a,A))) is M2( the carrier of K)
[a,A] is set
Indices M is set
[:(dom M),(Seg (width M)):] is set
a * M is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular FinSequence of the carrier of K *
width (a * M) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (a * M)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (a * M) ) } is set
len M is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len M ) } is set
Line ((a * M),a) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width (a * M)) FinSequence-like Element of (width (a * M)) -tuples_on the carrier of K
(width (a * M)) -tuples_on the carrier of K is functional V11() FinSequence-membered FinSequenceSet of the carrier of K
(Line ((a * M),a)) . A is set
(a * M) * (a,A) is M2( the carrier of K)
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
Seg n is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= n ) } is set
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
a is M2( the carrier of K)
a is V21() V22() V23() V27() ext-real non negative set
A is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
width A is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width A) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width A ) } is set
Line (A,a) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of K
(width A) -tuples_on the carrier of K is functional V11() FinSequence-membered FinSequenceSet of the carrier of K
M is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
M1 is V1() V4( NAT ) V5( the carrier of K) Function-like FinSequence-like FinSequence of the carrier of K
a * M1 is V1() V4( NAT ) V5( the carrier of K) Function-like FinSequence-like FinSequence of the carrier of K
a multfield is V1() V4( the carrier of K) V5( the carrier of K) Function-like V18( the carrier of K, the carrier of K) M2( bool [: the carrier of K, the carrier of K:])
[: the carrier of K, the carrier of K:] is set
bool [: the carrier of K, the carrier of K:] is set
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
K38( the carrier of K) is V1() V4( the carrier of K) V5( the carrier of K) V11() V14( the carrier of K) M2( bool [: the carrier of K, the carrier of K:])
K162( the carrier of K, the carrier of K, the multF of K,a,K38( the carrier of K)) is V1() V4( the carrier of K) V5( the carrier of K) Function-like V18( the carrier of K, the carrier of K) M2( bool [: the carrier of K, the carrier of K:])
K174( the carrier of K, the carrier of K,M1,(a multfield)) is V1() V4( NAT ) V5( the carrier of K) Function-like FinSequence-like FinSequence of the carrier of K
ReplaceLine (A,a,(a * M1)) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
M2 is V21() V22() V23() V27() ext-real non negative set
i is V21() V22() V23() V27() ext-real non negative set
M * (M2,i) is M2( the carrier of K)
A * (a,i) is M2( the carrier of K)
a * (A * (a,i)) is M2( the carrier of K)
the multF of K . (a,(A * (a,i))) is M2( the carrier of K)
A * (M2,i) is M2( the carrier of K)
len A is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom A is M2( bool NAT)
a * (Line (A,a)) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of K
K174( the carrier of K, the carrier of K,(Line (A,a)),(a multfield)) is V1() V4( NAT ) V5( the carrier of K) Function-like FinSequence-like FinSequence of the carrier of K
len (a * (Line (A,a))) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
Line (M,M2) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width M) FinSequence-like Element of (width M) -tuples_on the carrier of K
(width M) -tuples_on the carrier of K is functional V11() FinSequence-membered FinSequenceSet of the carrier of K
(Line (M,M2)) . i is set
(a * (Line (A,a))) . i is set
a * (Line (A,a)) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of K
K174( the carrier of K, the carrier of K,(Line (A,a)),(a multfield)) is V1() V4( NAT ) V5( the carrier of K) Function-like FinSequence-like FinSequence of the carrier of K
len (a * (Line (A,a))) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
Line (M,M2) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width M) FinSequence-like Element of (width M) -tuples_on the carrier of K
(width M) -tuples_on the carrier of K is functional V11() FinSequence-membered FinSequenceSet of the carrier of K
(Line (M,M2)) . i is set
Line (A,M2) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of K
(Line (A,M2)) . i is set
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
a is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len a is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom a is M2( bool NAT)
width a is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width a) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width a ) } is set
a is V21() V22() V23() V27() ext-real non negative set
A is M2( the carrier of K)
Line (a,a) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width a) FinSequence-like Element of (width a) -tuples_on the carrier of K
(width a) -tuples_on the carrier of K is functional V11() FinSequence-membered FinSequenceSet of the carrier of K
A * (Line (a,a)) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width a) FinSequence-like Element of (width a) -tuples_on the carrier of K
A multfield is V1() V4( the carrier of K) V5( the carrier of K) Function-like V18( the carrier of K, the carrier of K) M2( bool [: the carrier of K, the carrier of K:])
[: the carrier of K, the carrier of K:] is set
bool [: the carrier of K, the carrier of K:] is set
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
K38( the carrier of K) is V1() V4( the carrier of K) V5( the carrier of K) V11() V14( the carrier of K) M2( bool [: the carrier of K, the carrier of K:])
K162( the carrier of K, the carrier of K, the multF of K,A,K38( the carrier of K)) is V1() V4( the carrier of K) V5( the carrier of K) Function-like V18( the carrier of K, the carrier of K) M2( bool [: the carrier of K, the carrier of K:])
K174( the carrier of K, the carrier of K,(Line (a,a)),(A multfield)) is V1() V4( NAT ) V5( the carrier of K) Function-like FinSequence-like FinSequence of the carrier of K
ReplaceLine (a,a,(A * (Line (a,a)))) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len (ReplaceLine (a,a,(A * (Line (a,a))))) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg l is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= l ) } is set
len (Line (a,a)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (A * (Line (a,a))) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
M2 is V21() V22() V23() V27() ext-real non negative set
i is V21() V22() V23() V27() ext-real non negative set
(ReplaceLine (a,a,(A * (Line (a,a))))) * (M2,i) is M2( the carrier of K)
a * (a,i) is M2( the carrier of K)
A * (a * (a,i)) is M2( the carrier of K)
the multF of K . (A,(a * (a,i))) is M2( the carrier of K)
a * (M2,i) is M2( the carrier of K)
M is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
M1 is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Indices M is set
dom M is M2( bool NAT)
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Indices a is set
[:(dom a),(Seg (width a)):] is set
M2 is V21() V22() V23() V27() ext-real non negative set
i is V21() V22() V23() V27() ext-real non negative set
[M2,i] is set
M * (M2,i) is M2( the carrier of K)
M1 * (M2,i) is M2( the carrier of K)
a * (M2,i) is M2( the carrier of K)
a * (a,i) is M2( the carrier of K)
A * (a * (a,i)) is M2( the carrier of K)
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
[: the carrier of K, the carrier of K:] is set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the multF of K . (A,(a * (a,i))) is M2( the carrier of K)
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of a is V11() non trivial set
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
A is M2( the carrier of a)
M is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of a
dom M is M2( bool NAT)
(l,n,a,M,K,A) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of a
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
Line (M,K) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width M) FinSequence-like Element of (width M) -tuples_on the carrier of a
(width M) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
A * (Line (M,K)) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width M) FinSequence-like Element of (width M) -tuples_on the carrier of a
A multfield is V1() V4( the carrier of a) V5( the carrier of a) Function-like V18( the carrier of a, the carrier of a) M2( bool [: the carrier of a, the carrier of a:])
[: the carrier of a, the carrier of a:] is set
bool [: the carrier of a, the carrier of a:] is set
the multF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) V155( the carrier of a) M2( bool [:[: the carrier of a, the carrier of a:], the carrier of a:])
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
K38( the carrier of a) is V1() V4( the carrier of a) V5( the carrier of a) V11() V14( the carrier of a) M2( bool [: the carrier of a, the carrier of a:])
K162( the carrier of a, the carrier of a, the multF of a,A,K38( the carrier of a)) is V1() V4( the carrier of a) V5( the carrier of a) Function-like V18( the carrier of a, the carrier of a) M2( bool [: the carrier of a, the carrier of a:])
K174( the carrier of a, the carrier of a,(Line (M,K)),(A multfield)) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Line (M,a) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width M) FinSequence-like Element of (width M) -tuples_on the carrier of a
M1 is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of a
Line (M1,a) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width M1) FinSequence-like Element of (width M1) -tuples_on the carrier of a
width M1 is V21() V22() V23() V27() ext-real non negative M2( NAT )
(width M1) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
len (Line (M1,a)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
M2 is V21() V22() V23() V27() ext-real non negative set
Seg (width M1) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M1 ) } is set
(Line (M1,a)) . M2 is set
M1 * (a,M2) is M2( the carrier of a)
M * (K,M2) is M2( the carrier of a)
A * (M * (K,M2)) is M2( the carrier of a)
the multF of a . (A,(M * (K,M2))) is M2( the carrier of a)
(A * (Line (M,K))) . M2 is set
len (A * (Line (M,K))) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (Line (M,K)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (Line (M1,a)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
M2 is V21() V22() V23() V27() ext-real non negative set
Seg (width M1) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M1 ) } is set
(Line (M1,a)) . M2 is set
M1 * (a,M2) is M2( the carrier of a)
M * (a,M2) is M2( the carrier of a)
(Line (M,a)) . M2 is set
len (Line (M,a)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
Seg K is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= K ) } is set
a is V21() V22() V23() V27() ext-real non negative set
a is V21() V22() V23() V27() ext-real non negative set
A is V21() V22() V23() V27() ext-real non negative set
M is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of M is V11() non trivial set
the carrier of M * is functional FinSequence-membered FinSequenceSet of the carrier of M
M1 is M2( the carrier of M)
M2 is V1() V4( NAT ) V5( the carrier of M * ) Function-like FinSequence-like tabular Matrix of K,l, the carrier of M
width M2 is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width M2) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M2 ) } is set
dom M2 is M2( bool NAT)
Line (M2,A) is V1() V4( NAT ) V5( the carrier of M) Function-like V35( width M2) FinSequence-like Element of (width M2) -tuples_on the carrier of M
(width M2) -tuples_on the carrier of M is functional V11() FinSequence-membered FinSequenceSet of the carrier of M
Line (M2,a) is V1() V4( NAT ) V5( the carrier of M) Function-like V35( width M2) FinSequence-like Element of (width M2) -tuples_on the carrier of M
M2 * (a,a) is M2( the carrier of M)
M1 * (M2 * (a,a)) is M2( the carrier of M)
the multF of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) Function-like V18([: the carrier of M, the carrier of M:], the carrier of M) V155( the carrier of M) M2( bool [:[: the carrier of M, the carrier of M:], the carrier of M:])
[: the carrier of M, the carrier of M:] is set
[:[: the carrier of M, the carrier of M:], the carrier of M:] is set
bool [:[: the carrier of M, the carrier of M:], the carrier of M:] is set
the multF of M . (M1,(M2 * (a,a))) is M2( the carrier of M)
M2 * (A,a) is M2( the carrier of M)
(M1 * (M2 * (a,a))) + (M2 * (A,a)) is M2( the carrier of M)
the addF of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) Function-like V18([: the carrier of M, the carrier of M:], the carrier of M) V155( the carrier of M) V156( the carrier of M) M2( bool [:[: the carrier of M, the carrier of M:], the carrier of M:])
the addF of M . ((M1 * (M2 * (a,a))),(M2 * (A,a))) is M2( the carrier of M)
M2 * (n,a) is M2( the carrier of M)
i is V1() V4( NAT ) V5( the carrier of M * ) Function-like FinSequence-like tabular Matrix of K,l, the carrier of M
i * (n,a) is M2( the carrier of M)
j is V1() V4( NAT ) V5( the carrier of M) Function-like FinSequence-like FinSequence of the carrier of M
p1 is V1() V4( NAT ) V5( the carrier of M) Function-like FinSequence-like FinSequence of the carrier of M
M1 * p1 is V1() V4( NAT ) V5( the carrier of M) Function-like FinSequence-like FinSequence of the carrier of M
M1 multfield is V1() V4( the carrier of M) V5( the carrier of M) Function-like V18( the carrier of M, the carrier of M) M2( bool [: the carrier of M, the carrier of M:])
bool [: the carrier of M, the carrier of M:] is set
K38( the carrier of M) is V1() V4( the carrier of M) V5( the carrier of M) V11() V14( the carrier of M) M2( bool [: the carrier of M, the carrier of M:])
K162( the carrier of M, the carrier of M, the multF of M,M1,K38( the carrier of M)) is V1() V4( the carrier of M) V5( the carrier of M) Function-like V18( the carrier of M, the carrier of M) M2( bool [: the carrier of M, the carrier of M:])
K174( the carrier of M, the carrier of M,p1,(M1 multfield)) is V1() V4( NAT ) V5( the carrier of M) Function-like FinSequence-like FinSequence of the carrier of M
(M1 * p1) + j is V1() V4( NAT ) V5( the carrier of M) Function-like FinSequence-like FinSequence of the carrier of M
K171( the carrier of M, the carrier of M, the carrier of M, the addF of M,(M1 * p1),j) is V1() V4( NAT ) V5( the carrier of M) Function-like FinSequence-like FinSequence of the carrier of M
ReplaceLine (M2,A,((M1 * p1) + j)) is V1() V4( NAT ) V5( the carrier of M * ) Function-like FinSequence-like tabular Matrix of K,l, the carrier of M
M1 * (Line (M2,a)) is V1() V4( NAT ) V5( the carrier of M) Function-like V35( width M2) FinSequence-like Element of (width M2) -tuples_on the carrier of M
K174( the carrier of M, the carrier of M,(Line (M2,a)),(M1 multfield)) is V1() V4( NAT ) V5( the carrier of M) Function-like FinSequence-like FinSequence of the carrier of M
(M1 * (Line (M2,a))) . a is set
a1 is M2( the carrier of M)
(Line (M2,A)) . a is set
a2 is M2( the carrier of M)
len ((M1 * p1) + j) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom ((M1 * p1) + j) is M2( bool NAT)
((M1 * p1) + j) . a is set
the addF of M . (a1,a2) is M2( the carrier of M)
width i is V21() V22() V23() V27() ext-real non negative M2( NAT )
Line (i,n) is V1() V4( NAT ) V5( the carrier of M) Function-like V35( width i) FinSequence-like Element of (width i) -tuples_on the carrier of M
(width i) -tuples_on the carrier of M is functional V11() FinSequence-membered FinSequenceSet of the carrier of M
(Line (i,n)) . a is set
len ((M1 * p1) + j) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width i is V21() V22() V23() V27() ext-real non negative M2( NAT )
Line (i,n) is V1() V4( NAT ) V5( the carrier of M) Function-like V35( width i) FinSequence-like Element of (width i) -tuples_on the carrier of M
(width i) -tuples_on the carrier of M is functional V11() FinSequence-membered FinSequenceSet of the carrier of M
(Line (i,n)) . a is set
Line (M2,n) is V1() V4( NAT ) V5( the carrier of M) Function-like V35( width M2) FinSequence-like Element of (width M2) -tuples_on the carrier of M
(Line (M2,n)) . a is set
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
A is V21() V22() V23() V27() ext-real non negative set
a is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
dom a is M2( bool NAT)
len a is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width a is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width a) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width a ) } is set
a is V21() V22() V23() V27() ext-real non negative set
M is M2( the carrier of K)
Line (a,A) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width a) FinSequence-like Element of (width a) -tuples_on the carrier of K
(width a) -tuples_on the carrier of K is functional V11() FinSequence-membered FinSequenceSet of the carrier of K
Line (a,a) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width a) FinSequence-like Element of (width a) -tuples_on the carrier of K
M * (Line (a,A)) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width a) FinSequence-like Element of (width a) -tuples_on the carrier of K
M multfield is V1() V4( the carrier of K) V5( the carrier of K) Function-like V18( the carrier of K, the carrier of K) M2( bool [: the carrier of K, the carrier of K:])
[: the carrier of K, the carrier of K:] is set
bool [: the carrier of K, the carrier of K:] is set
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
K38( the carrier of K) is V1() V4( the carrier of K) V5( the carrier of K) V11() V14( the carrier of K) M2( bool [: the carrier of K, the carrier of K:])
K162( the carrier of K, the carrier of K, the multF of K,M,K38( the carrier of K)) is V1() V4( the carrier of K) V5( the carrier of K) Function-like V18( the carrier of K, the carrier of K) M2( bool [: the carrier of K, the carrier of K:])
K174( the carrier of K, the carrier of K,(Line (a,A)),(M multfield)) is V1() V4( NAT ) V5( the carrier of K) Function-like FinSequence-like FinSequence of the carrier of K
(M * (Line (a,A))) + (Line (a,a)) is V1() V4( NAT ) V5( the carrier of K) Function-like V35( width a) FinSequence-like Element of (width a) -tuples_on the carrier of K
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) V156( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
K171( the carrier of K, the carrier of K, the carrier of K, the addF of K,(M * (Line (a,A))),(Line (a,a))) is V1() V4( NAT ) V5( the carrier of K) Function-like FinSequence-like FinSequence of the carrier of K
ReplaceLine (a,a,((M * (Line (a,A))) + (Line (a,a)))) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len (ReplaceLine (a,a,((M * (Line (a,A))) + (Line (a,a))))) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len ((M * (Line (a,A))) + (Line (a,a))) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg l is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= l ) } is set
j is V21() V22() V23() V27() ext-real non negative set
p1 is V21() V22() V23() V27() ext-real non negative set
(ReplaceLine (a,a,((M * (Line (a,A))) + (Line (a,a))))) * (j,p1) is M2( the carrier of K)
a * (A,p1) is M2( the carrier of K)
M * (a * (A,p1)) is M2( the carrier of K)
the multF of K . (M,(a * (A,p1))) is M2( the carrier of K)
a * (a,p1) is M2( the carrier of K)
(M * (a * (A,p1))) + (a * (a,p1)) is M2( the carrier of K)
the addF of K . ((M * (a * (A,p1))),(a * (a,p1))) is M2( the carrier of K)
a * (j,p1) is M2( the carrier of K)
M1 is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
M2 is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M2 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Indices M1 is set
dom M1 is M2( bool NAT)
width M1 is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width M1) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M1 ) } is set
[:(dom M1),(Seg (width M1)):] is set
Indices a is set
[:(dom a),(Seg (width a)):] is set
i is V21() V22() V23() V27() ext-real non negative set
j is V21() V22() V23() V27() ext-real non negative set
[i,j] is set
M1 * (i,j) is M2( the carrier of K)
M2 * (i,j) is M2( the carrier of K)
a * (i,j) is M2( the carrier of K)
a * (A,j) is M2( the carrier of K)
M * (a * (A,j)) is M2( the carrier of K)
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
[: the carrier of K, the carrier of K:] is set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the multF of K . (M,(a * (A,j))) is M2( the carrier of K)
a * (a,j) is M2( the carrier of K)
(M * (a * (A,j))) + (a * (a,j)) is M2( the carrier of K)
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) V156( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
the addF of K . ((M * (a * (A,j))),(a * (a,j))) is M2( the carrier of K)
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V21() V22() V23() V27() ext-real non negative set
a is V21() V22() V23() V27() ext-real non negative set
A is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of A is V11() non trivial set
the carrier of A * is functional FinSequence-membered FinSequenceSet of the carrier of A
M is M2( the carrier of A)
M1 is V1() V4( NAT ) V5( the carrier of A * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of A
dom M1 is M2( bool NAT)
(l,n,A,M1,K,a,M) is V1() V4( NAT ) V5( the carrier of A * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of A
width M1 is V21() V22() V23() V27() ext-real non negative M2( NAT )
Line (M1,a) is V1() V4( NAT ) V5( the carrier of A) Function-like V35( width M1) FinSequence-like Element of (width M1) -tuples_on the carrier of A
(width M1) -tuples_on the carrier of A is functional V11() FinSequence-membered FinSequenceSet of the carrier of A
M * (Line (M1,a)) is V1() V4( NAT ) V5( the carrier of A) Function-like V35( width M1) FinSequence-like Element of (width M1) -tuples_on the carrier of A
M multfield is V1() V4( the carrier of A) V5( the carrier of A) Function-like V18( the carrier of A, the carrier of A) M2( bool [: the carrier of A, the carrier of A:])
[: the carrier of A, the carrier of A:] is set
bool [: the carrier of A, the carrier of A:] is set
the multF of A is V1() V4([: the carrier of A, the carrier of A:]) V5( the carrier of A) Function-like V18([: the carrier of A, the carrier of A:], the carrier of A) V155( the carrier of A) M2( bool [:[: the carrier of A, the carrier of A:], the carrier of A:])
[:[: the carrier of A, the carrier of A:], the carrier of A:] is set
bool [:[: the carrier of A, the carrier of A:], the carrier of A:] is set
K38( the carrier of A) is V1() V4( the carrier of A) V5( the carrier of A) V11() V14( the carrier of A) M2( bool [: the carrier of A, the carrier of A:])
K162( the carrier of A, the carrier of A, the multF of A,M,K38( the carrier of A)) is V1() V4( the carrier of A) V5( the carrier of A) Function-like V18( the carrier of A, the carrier of A) M2( bool [: the carrier of A, the carrier of A:])
K174( the carrier of A, the carrier of A,(Line (M1,a)),(M multfield)) is V1() V4( NAT ) V5( the carrier of A) Function-like FinSequence-like FinSequence of the carrier of A
Line (M1,K) is V1() V4( NAT ) V5( the carrier of A) Function-like V35( width M1) FinSequence-like Element of (width M1) -tuples_on the carrier of A
(M * (Line (M1,a))) + (Line (M1,K)) is V1() V4( NAT ) V5( the carrier of A) Function-like V35( width M1) FinSequence-like Element of (width M1) -tuples_on the carrier of A
the addF of A is V1() V4([: the carrier of A, the carrier of A:]) V5( the carrier of A) Function-like V18([: the carrier of A, the carrier of A:], the carrier of A) V155( the carrier of A) V156( the carrier of A) M2( bool [:[: the carrier of A, the carrier of A:], the carrier of A:])
K171( the carrier of A, the carrier of A, the carrier of A, the addF of A,(M * (Line (M1,a))),(Line (M1,K))) is V1() V4( NAT ) V5( the carrier of A) Function-like FinSequence-like FinSequence of the carrier of A
Line (M1,a) is V1() V4( NAT ) V5( the carrier of A) Function-like V35( width M1) FinSequence-like Element of (width M1) -tuples_on the carrier of A
M2 is V1() V4( NAT ) V5( the carrier of A * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of A
Line (M2,a) is V1() V4( NAT ) V5( the carrier of A) Function-like V35( width M2) FinSequence-like Element of (width M2) -tuples_on the carrier of A
width M2 is V21() V22() V23() V27() ext-real non negative M2( NAT )
(width M2) -tuples_on the carrier of A is functional V11() FinSequence-membered FinSequenceSet of the carrier of A
len ((M * (Line (M1,a))) + (Line (M1,K))) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (Line (M2,a)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
i is V21() V22() V23() V27() ext-real non negative set
Seg (width M2) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M2 ) } is set
(Line (M1,K)) . i is set
M1 * (K,i) is M2( the carrier of A)
j is M2( the carrier of A)
(M * (Line (M1,a))) . i is set
M1 * (a,i) is M2( the carrier of A)
M * (M1 * (a,i)) is M2( the carrier of A)
the multF of A . (M,(M1 * (a,i))) is M2( the carrier of A)
p1 is M2( the carrier of A)
dom ((M * (Line (M1,a))) + (Line (M1,K))) is M2( bool NAT)
((M * (Line (M1,a))) + (Line (M1,K))) . i is set
the addF of A . (p1,j) is M2( the carrier of A)
(M * (M1 * (a,i))) + (M1 * (K,i)) is M2( the carrier of A)
the addF of A . ((M * (M1 * (a,i))),(M1 * (K,i))) is M2( the carrier of A)
(Line (M2,a)) . i is set
M2 * (a,i) is M2( the carrier of A)
len (Line (M2,a)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
i is V21() V22() V23() V27() ext-real non negative set
Seg (width M2) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M2 ) } is set
(Line (M2,a)) . i is set
M2 * (a,i) is M2( the carrier of A)
M1 * (a,i) is M2( the carrier of A)
(Line (M1,a)) . i is set
len (Line (M1,a)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of a is V11() non trivial set
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
1. (a,n) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
dom (1. (a,n)) is M2( bool NAT)
(n,n,a,(1. (a,n)),l,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
a is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K) * a is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,a,l,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
len (n,n,a,(1. (a,n)),l,K) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (1. (a,n)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg n is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= n ) } is set
width (n,n,a,(1. (a,n)),l,K) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Indices ((n,n,a,(1. (a,n)),l,K) * a) is set
dom ((n,n,a,(1. (a,n)),l,K) * a) is M2( bool NAT)
width ((n,n,a,(1. (a,n)),l,K) * a) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width ((n,n,a,(1. (a,n)),l,K) * a)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width ((n,n,a,(1. (a,n)),l,K) * a) ) } is set
[:(dom ((n,n,a,(1. (a,n)),l,K) * a)),(Seg (width ((n,n,a,(1. (a,n)),l,K) * a))):] is set
[:(Seg n),(Seg n):] is set
width a is V21() V22() V23() V27() ext-real non negative M2( NAT )
len a is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (1. (a,n)) is V21() V22() V23() V27() ext-real non negative M2( NAT )
M is V21() V22() V23() V27() ext-real non negative set
M1 is V21() V22() V23() V27() ext-real non negative set
((n,n,a,(1. (a,n)),l,K) * a) * (M,M1) is M2( the carrier of a)
(n,n,a,a,l,K) * (M,M1) is M2( the carrier of a)
[M,M] is set
Indices (1. (a,n)) is set
Seg (width (1. (a,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (1. (a,n)) ) } is set
[:(dom (1. (a,n))),(Seg (width (1. (a,n)))):] is set
Line ((1. (a,n)),M) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width (1. (a,n))) FinSequence-like Element of (width (1. (a,n))) -tuples_on the carrier of a
(width (1. (a,n))) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
(Line ((1. (a,n)),M)) . M is set
1_ a is M2( the carrier of a)
1. a is V47(a) M2( the carrier of a)
dom (Line ((1. (a,n)),M)) is M2( bool NAT)
0. a is V47(a) M2( the carrier of a)
M2 is V21() V22() V23() V27() ext-real non negative set
(Line ((1. (a,n)),M)) . M2 is set
len (Line ((1. (a,n)),M)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len (Line ((1. (a,n)),M))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (Line ((1. (a,n)),M)) ) } is set
[M,M2] is set
Col (a,M1) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( len a) FinSequence-like Element of (len a) -tuples_on the carrier of a
(len a) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
len (Col (a,M1)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom (Col (a,M1)) is M2( bool NAT)
Seg (len (1. (a,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (1. (a,n)) ) } is set
Seg (len a) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len a ) } is set
dom a is M2( bool NAT)
len (Line ((1. (a,n)),M)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
[M,M1] is set
Line ((n,n,a,(1. (a,n)),l,K),M) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width (n,n,a,(1. (a,n)),l,K)) FinSequence-like Element of (width (n,n,a,(1. (a,n)),l,K)) -tuples_on the carrier of a
(width (n,n,a,(1. (a,n)),l,K)) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
(Line ((n,n,a,(1. (a,n)),l,K),M)) "*" (Col (a,M1)) is M2( the carrier of a)
mlt ((Line ((n,n,a,(1. (a,n)),l,K),M)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
the multF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) V155( the carrier of a) M2( bool [:[: the carrier of a, the carrier of a:], the carrier of a:])
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,(Line ((n,n,a,(1. (a,n)),l,K),M)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Sum (mlt ((Line ((n,n,a,(1. (a,n)),l,K),M)),(Col (a,M1)))) is M2( the carrier of a)
mlt ((Line ((1. (a,n)),M)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,(Line ((1. (a,n)),M)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Sum (mlt ((Line ((1. (a,n)),M)),(Col (a,M1)))) is M2( the carrier of a)
(Col (a,M1)) . M is set
a * (M,M1) is M2( the carrier of a)
Seg (width (1. (a,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (1. (a,n)) ) } is set
[l,l] is set
Indices (1. (a,n)) is set
[:(dom (1. (a,n))),(Seg (width (1. (a,n)))):] is set
M is V21() V22() V23() V27() ext-real non negative set
M1 is V21() V22() V23() V27() ext-real non negative set
((n,n,a,(1. (a,n)),l,K) * a) * (M,M1) is M2( the carrier of a)
(n,n,a,a,l,K) * (M,M1) is M2( the carrier of a)
Line ((1. (a,n)),l) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width (1. (a,n))) FinSequence-like Element of (width (1. (a,n))) -tuples_on the carrier of a
(width (1. (a,n))) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
(Line ((1. (a,n)),l)) . l is set
1_ a is M2( the carrier of a)
1. a is V47(a) M2( the carrier of a)
dom (Line ((1. (a,n)),l)) is M2( bool NAT)
0. a is V47(a) M2( the carrier of a)
M2 is V21() V22() V23() V27() ext-real non negative set
(Line ((1. (a,n)),l)) . M2 is set
len (Line ((1. (a,n)),l)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len (Line ((1. (a,n)),l))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (Line ((1. (a,n)),l)) ) } is set
[l,M2] is set
len (Line ((1. (a,n)),l)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Col (a,M1) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( len a) FinSequence-like Element of (len a) -tuples_on the carrier of a
(len a) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
len (Col (a,M1)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom (Col (a,M1)) is M2( bool NAT)
Seg (len (1. (a,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (1. (a,n)) ) } is set
Seg (len a) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len a ) } is set
dom a is M2( bool NAT)
[M,M1] is set
Line ((n,n,a,(1. (a,n)),l,K),M) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width (n,n,a,(1. (a,n)),l,K)) FinSequence-like Element of (width (n,n,a,(1. (a,n)),l,K)) -tuples_on the carrier of a
(width (n,n,a,(1. (a,n)),l,K)) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
(Line ((n,n,a,(1. (a,n)),l,K),M)) "*" (Col (a,M1)) is M2( the carrier of a)
mlt ((Line ((n,n,a,(1. (a,n)),l,K),M)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
the multF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) V155( the carrier of a) M2( bool [:[: the carrier of a, the carrier of a:], the carrier of a:])
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,(Line ((n,n,a,(1. (a,n)),l,K),M)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Sum (mlt ((Line ((n,n,a,(1. (a,n)),l,K),M)),(Col (a,M1)))) is M2( the carrier of a)
mlt ((Line ((1. (a,n)),l)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,(Line ((1. (a,n)),l)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Sum (mlt ((Line ((1. (a,n)),l)),(Col (a,M1)))) is M2( the carrier of a)
(Col (a,M1)) . l is set
a * (l,M1) is M2( the carrier of a)
[K,K] is set
M is V21() V22() V23() V27() ext-real non negative set
M1 is V21() V22() V23() V27() ext-real non negative set
((n,n,a,(1. (a,n)),l,K) * a) * (M,M1) is M2( the carrier of a)
(n,n,a,a,l,K) * (M,M1) is M2( the carrier of a)
Line ((1. (a,n)),K) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width (1. (a,n))) FinSequence-like Element of (width (1. (a,n))) -tuples_on the carrier of a
(width (1. (a,n))) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
(Line ((1. (a,n)),K)) . K is set
1_ a is M2( the carrier of a)
1. a is V47(a) M2( the carrier of a)
dom (Line ((1. (a,n)),K)) is M2( bool NAT)
0. a is V47(a) M2( the carrier of a)
M2 is V21() V22() V23() V27() ext-real non negative set
(Line ((1. (a,n)),K)) . M2 is set
len (Line ((1. (a,n)),K)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len (Line ((1. (a,n)),K))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (Line ((1. (a,n)),K)) ) } is set
[K,M2] is set
len (Line ((1. (a,n)),K)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Col (a,M1) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( len a) FinSequence-like Element of (len a) -tuples_on the carrier of a
(len a) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
len (Col (a,M1)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom (Col (a,M1)) is M2( bool NAT)
Seg (len (1. (a,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (1. (a,n)) ) } is set
Seg (len a) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len a ) } is set
dom a is M2( bool NAT)
[M,M1] is set
Line ((n,n,a,(1. (a,n)),l,K),M) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width (n,n,a,(1. (a,n)),l,K)) FinSequence-like Element of (width (n,n,a,(1. (a,n)),l,K)) -tuples_on the carrier of a
(width (n,n,a,(1. (a,n)),l,K)) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
(Line ((n,n,a,(1. (a,n)),l,K),M)) "*" (Col (a,M1)) is M2( the carrier of a)
mlt ((Line ((n,n,a,(1. (a,n)),l,K),M)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
the multF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) V155( the carrier of a) M2( bool [:[: the carrier of a, the carrier of a:], the carrier of a:])
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,(Line ((n,n,a,(1. (a,n)),l,K),M)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Sum (mlt ((Line ((n,n,a,(1. (a,n)),l,K),M)),(Col (a,M1)))) is M2( the carrier of a)
mlt ((Line ((1. (a,n)),K)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,(Line ((1. (a,n)),K)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Sum (mlt ((Line ((1. (a,n)),K)),(Col (a,M1)))) is M2( the carrier of a)
(Col (a,M1)) . K is set
a * (K,M1) is M2( the carrier of a)
M is V21() V22() V23() V27() ext-real non negative set
M1 is V21() V22() V23() V27() ext-real non negative set
[M,M1] is set
((n,n,a,(1. (a,n)),l,K) * a) * (M,M1) is M2( the carrier of a)
(n,n,a,a,l,K) * (M,M1) is M2( the carrier of a)
Seg (len (1. (a,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (1. (a,n)) ) } is set
len ((n,n,a,(1. (a,n)),l,K) * a) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (n,n,a,a,l,K) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (n,n,a,a,l,K) is V21() V22() V23() V27() ext-real non negative M2( NAT )
l is V21() V22() V23() V27() ext-real non negative set
n is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of n is V11() non trivial set
the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n
1. (n,l) is V1() V4( NAT ) V5( the carrier of n * ) Function-like FinSequence-like tabular Matrix of l,l, the carrier of n
dom (1. (n,l)) is M2( bool NAT)
K is V21() V22() V23() V27() ext-real non negative set
a is M2( the carrier of n)
(l,l,n,(1. (n,l)),K,a) is V1() V4( NAT ) V5( the carrier of n * ) Function-like FinSequence-like tabular Matrix of l,l, the carrier of n
a is V1() V4( NAT ) V5( the carrier of n * ) Function-like FinSequence-like tabular Matrix of l,l, the carrier of n
(l,l,n,(1. (n,l)),K,a) * a is V1() V4( NAT ) V5( the carrier of n * ) Function-like FinSequence-like tabular Matrix of l,l, the carrier of n
(l,l,n,a,K,a) is V1() V4( NAT ) V5( the carrier of n * ) Function-like FinSequence-like tabular Matrix of l,l, the carrier of n
len (l,l,n,(1. (n,l)),K,a) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (1. (n,l)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg l is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= l ) } is set
width (l,l,n,(1. (n,l)),K,a) is V21() V22() V23() V27() ext-real non negative M2( NAT )
width a is V21() V22() V23() V27() ext-real non negative M2( NAT )
len a is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Indices ((l,l,n,(1. (n,l)),K,a) * a) is set
dom ((l,l,n,(1. (n,l)),K,a) * a) is M2( bool NAT)
width ((l,l,n,(1. (n,l)),K,a) * a) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width ((l,l,n,(1. (n,l)),K,a) * a)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width ((l,l,n,(1. (n,l)),K,a) * a) ) } is set
[:(dom ((l,l,n,(1. (n,l)),K,a) * a)),(Seg (width ((l,l,n,(1. (n,l)),K,a) * a))):] is set
[:(Seg l),(Seg l):] is set
width (1. (n,l)) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (1. (n,l))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (1. (n,l)) ) } is set
[K,K] is set
Indices (1. (n,l)) is set
[:(dom (1. (n,l))),(Seg (width (1. (n,l)))):] is set
M is V21() V22() V23() V27() ext-real non negative set
M1 is V21() V22() V23() V27() ext-real non negative set
((l,l,n,(1. (n,l)),K,a) * a) * (M,M1) is M2( the carrier of n)
(l,l,n,a,K,a) * (M,M1) is M2( the carrier of n)
(width a) -tuples_on the carrier of n is functional V11() FinSequence-membered FinSequenceSet of the carrier of n
Line ((1. (n,l)),K) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (1. (n,l))) FinSequence-like Element of (width (1. (n,l))) -tuples_on the carrier of n
(width (1. (n,l))) -tuples_on the carrier of n is functional V11() FinSequence-membered FinSequenceSet of the carrier of n
Col (a,M1) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( len a) FinSequence-like Element of (len a) -tuples_on the carrier of n
(len a) -tuples_on the carrier of n is functional V11() FinSequence-membered FinSequenceSet of the carrier of n
len (Line ((1. (n,l)),K)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom (Line ((1. (n,l)),K)) is M2( bool NAT)
len (Col (a,M1)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom (Col (a,M1)) is M2( bool NAT)
(Line ((1. (n,l)),K)) . K is set
1_ n is M2( the carrier of n)
1. n is V47(n) M2( the carrier of n)
0. n is V47(n) M2( the carrier of n)
j is V21() V22() V23() V27() ext-real non negative set
(Line ((1. (n,l)),K)) . j is set
Seg (len (Line ((1. (n,l)),K))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (Line ((1. (n,l)),K)) ) } is set
[K,j] is set
Seg (len (1. (n,l))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (1. (n,l)) ) } is set
Seg (len a) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len a ) } is set
dom a is M2( bool NAT)
(Col (a,M1)) . K is set
a * (K,M1) is M2( the carrier of n)
j is M2( the carrier of n)
[M,M1] is set
Line ((l,l,n,(1. (n,l)),K,a),M) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),K,a)) FinSequence-like Element of (width (l,l,n,(1. (n,l)),K,a)) -tuples_on the carrier of n
(width (l,l,n,(1. (n,l)),K,a)) -tuples_on the carrier of n is functional V11() FinSequence-membered FinSequenceSet of the carrier of n
(Line ((l,l,n,(1. (n,l)),K,a),M)) "*" (Col (a,M1)) is M2( the carrier of n)
mlt ((Line ((l,l,n,(1. (n,l)),K,a),M)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
the multF of n is V1() V4([: the carrier of n, the carrier of n:]) V5( the carrier of n) Function-like V18([: the carrier of n, the carrier of n:], the carrier of n) V155( the carrier of n) M2( bool [:[: the carrier of n, the carrier of n:], the carrier of n:])
[: the carrier of n, the carrier of n:] is set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set
K171( the carrier of n, the carrier of n, the carrier of n, the multF of n,(Line ((l,l,n,(1. (n,l)),K,a),M)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
Sum (mlt ((Line ((l,l,n,(1. (n,l)),K,a),M)),(Col (a,M1)))) is M2( the carrier of n)
M2 is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width a) FinSequence-like Element of (width a) -tuples_on the carrier of n
a * M2 is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width a) FinSequence-like Element of (width a) -tuples_on the carrier of n
a multfield is V1() V4( the carrier of n) V5( the carrier of n) Function-like V18( the carrier of n, the carrier of n) M2( bool [: the carrier of n, the carrier of n:])
bool [: the carrier of n, the carrier of n:] is set
K38( the carrier of n) is V1() V4( the carrier of n) V5( the carrier of n) V11() V14( the carrier of n) M2( bool [: the carrier of n, the carrier of n:])
K162( the carrier of n, the carrier of n, the multF of n,a,K38( the carrier of n)) is V1() V4( the carrier of n) V5( the carrier of n) Function-like V18( the carrier of n, the carrier of n) M2( bool [: the carrier of n, the carrier of n:])
K174( the carrier of n, the carrier of n,M2,(a multfield)) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
i is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width a) FinSequence-like Element of (width a) -tuples_on the carrier of n
mlt ((a * M2),i) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width a) FinSequence-like Element of (width a) -tuples_on the carrier of n
K171( the carrier of n, the carrier of n, the carrier of n, the multF of n,(a * M2),i) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
Sum (mlt ((a * M2),i)) is M2( the carrier of n)
mlt (M2,i) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width a) FinSequence-like Element of (width a) -tuples_on the carrier of n
K171( the carrier of n, the carrier of n, the carrier of n, the multF of n,M2,i) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
a * (mlt (M2,i)) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width a) FinSequence-like Element of (width a) -tuples_on the carrier of n
K174( the carrier of n, the carrier of n,(mlt (M2,i)),(a multfield)) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
Sum (a * (mlt (M2,i))) is M2( the carrier of n)
mlt ((Line ((1. (n,l)),K)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
K171( the carrier of n, the carrier of n, the carrier of n, the multF of n,(Line ((1. (n,l)),K)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
Sum (mlt ((Line ((1. (n,l)),K)),(Col (a,M1)))) is M2( the carrier of n)
a * (Sum (mlt ((Line ((1. (n,l)),K)),(Col (a,M1))))) is M2( the carrier of n)
the multF of n . (a,(Sum (mlt ((Line ((1. (n,l)),K)),(Col (a,M1)))))) is M2( the carrier of n)
a * j is M2( the carrier of n)
the multF of n . (a,j) is M2( the carrier of n)
a * (a * (K,M1)) is M2( the carrier of n)
the multF of n . (a,(a * (K,M1))) is M2( the carrier of n)
M is V21() V22() V23() V27() ext-real non negative set
M1 is V21() V22() V23() V27() ext-real non negative set
((l,l,n,(1. (n,l)),K,a) * a) * (M,M1) is M2( the carrier of n)
(l,l,n,a,K,a) * (M,M1) is M2( the carrier of n)
[M,M] is set
Line ((1. (n,l)),M) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (1. (n,l))) FinSequence-like Element of (width (1. (n,l))) -tuples_on the carrier of n
(width (1. (n,l))) -tuples_on the carrier of n is functional V11() FinSequence-membered FinSequenceSet of the carrier of n
(Line ((1. (n,l)),M)) . M is set
1_ n is M2( the carrier of n)
1. n is V47(n) M2( the carrier of n)
dom (Line ((1. (n,l)),M)) is M2( bool NAT)
0. n is V47(n) M2( the carrier of n)
M2 is V21() V22() V23() V27() ext-real non negative set
(Line ((1. (n,l)),M)) . M2 is set
len (Line ((1. (n,l)),M)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len (Line ((1. (n,l)),M))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (Line ((1. (n,l)),M)) ) } is set
[M,M2] is set
Col (a,M1) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( len a) FinSequence-like Element of (len a) -tuples_on the carrier of n
(len a) -tuples_on the carrier of n is functional V11() FinSequence-membered FinSequenceSet of the carrier of n
len (Col (a,M1)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom (Col (a,M1)) is M2( bool NAT)
Seg (len (1. (n,l))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (1. (n,l)) ) } is set
Seg (len a) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len a ) } is set
dom a is M2( bool NAT)
len (Line ((1. (n,l)),M)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
[M,M1] is set
Line ((l,l,n,(1. (n,l)),K,a),M) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),K,a)) FinSequence-like Element of (width (l,l,n,(1. (n,l)),K,a)) -tuples_on the carrier of n
(width (l,l,n,(1. (n,l)),K,a)) -tuples_on the carrier of n is functional V11() FinSequence-membered FinSequenceSet of the carrier of n
(Line ((l,l,n,(1. (n,l)),K,a),M)) "*" (Col (a,M1)) is M2( the carrier of n)
mlt ((Line ((l,l,n,(1. (n,l)),K,a),M)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
the multF of n is V1() V4([: the carrier of n, the carrier of n:]) V5( the carrier of n) Function-like V18([: the carrier of n, the carrier of n:], the carrier of n) V155( the carrier of n) M2( bool [:[: the carrier of n, the carrier of n:], the carrier of n:])
[: the carrier of n, the carrier of n:] is set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set
K171( the carrier of n, the carrier of n, the carrier of n, the multF of n,(Line ((l,l,n,(1. (n,l)),K,a),M)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
Sum (mlt ((Line ((l,l,n,(1. (n,l)),K,a),M)),(Col (a,M1)))) is M2( the carrier of n)
mlt ((Line ((1. (n,l)),M)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
K171( the carrier of n, the carrier of n, the carrier of n, the multF of n,(Line ((1. (n,l)),M)),(Col (a,M1))) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
Sum (mlt ((Line ((1. (n,l)),M)),(Col (a,M1)))) is M2( the carrier of n)
(Col (a,M1)) . M is set
a * (M,M1) is M2( the carrier of n)
M is V21() V22() V23() V27() ext-real non negative set
M1 is V21() V22() V23() V27() ext-real non negative set
[M,M1] is set
((l,l,n,(1. (n,l)),K,a) * a) * (M,M1) is M2( the carrier of n)
(l,l,n,a,K,a) * (M,M1) is M2( the carrier of n)
Seg (len (1. (n,l))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (1. (n,l)) ) } is set
len ((l,l,n,(1. (n,l)),K,a) * a) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (l,l,n,a,K,a) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (l,l,n,a,K,a) is V21() V22() V23() V27() ext-real non negative M2( NAT )
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of a is V11() non trivial set
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
1. (a,n) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
dom (1. (a,n)) is M2( bool NAT)
a is M2( the carrier of a)
(n,n,a,(1. (a,n)),l,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
A is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K,a) * A is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,A,l,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
len (n,n,a,(1. (a,n)),l,K,a) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len A is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (1. (a,n)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len (1. (a,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (1. (a,n)) ) } is set
Seg (len A) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len A ) } is set
dom A is M2( bool NAT)
len (n,n,a,A,l,K,a) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len ((n,n,a,(1. (a,n)),l,K,a) * A) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width ((n,n,a,(1. (a,n)),l,K,a) * A) is V21() V22() V23() V27() ext-real non negative M2( NAT )
width A is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg n is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= n ) } is set
width (n,n,a,(1. (a,n)),l,K,a) is V21() V22() V23() V27() ext-real non negative M2( NAT )
width (1. (a,n)) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (1. (a,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (1. (a,n)) ) } is set
[l,l] is set
Indices (1. (a,n)) is set
[:(dom (1. (a,n))),(Seg (width (1. (a,n)))):] is set
Indices ((n,n,a,(1. (a,n)),l,K,a) * A) is set
dom ((n,n,a,(1. (a,n)),l,K,a) * A) is M2( bool NAT)
Seg (width ((n,n,a,(1. (a,n)),l,K,a) * A)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width ((n,n,a,(1. (a,n)),l,K,a) * A) ) } is set
[:(dom ((n,n,a,(1. (a,n)),l,K,a) * A)),(Seg (width ((n,n,a,(1. (a,n)),l,K,a) * A))):] is set
[:(Seg n),(Seg n):] is set
[K,K] is set
M1 is V21() V22() V23() V27() ext-real non negative set
M2 is V21() V22() V23() V27() ext-real non negative set
((n,n,a,(1. (a,n)),l,K,a) * A) * (M1,M2) is M2( the carrier of a)
(n,n,a,A,l,K,a) * (M1,M2) is M2( the carrier of a)
Line ((1. (a,n)),l) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width (1. (a,n))) FinSequence-like Element of (width (1. (a,n))) -tuples_on the carrier of a
(width (1. (a,n))) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
(Line ((1. (a,n)),l)) . l is set
1_ a is M2( the carrier of a)
1. a is V47(a) M2( the carrier of a)
dom (Line ((1. (a,n)),l)) is M2( bool NAT)
0. a is V47(a) M2( the carrier of a)
i is V21() V22() V23() V27() ext-real non negative set
(Line ((1. (a,n)),l)) . i is set
len (Line ((1. (a,n)),l)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len (Line ((1. (a,n)),l))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (Line ((1. (a,n)),l)) ) } is set
[l,i] is set
(width A) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
Col (A,M2) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( len A) FinSequence-like Element of (len A) -tuples_on the carrier of a
(len A) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
len (Col (A,M2)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom (Col (A,M2)) is M2( bool NAT)
Line ((1. (a,n)),K) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width (1. (a,n))) FinSequence-like Element of (width (1. (a,n))) -tuples_on the carrier of a
len (Line ((1. (a,n)),K)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom (Line ((1. (a,n)),K)) is M2( bool NAT)
len (Line ((1. (a,n)),l)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
i is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
len i is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
p1 is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
a * p1 is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
a multfield is V1() V4( the carrier of a) V5( the carrier of a) Function-like V18( the carrier of a, the carrier of a) M2( bool [: the carrier of a, the carrier of a:])
[: the carrier of a, the carrier of a:] is set
bool [: the carrier of a, the carrier of a:] is set
the multF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) V155( the carrier of a) M2( bool [:[: the carrier of a, the carrier of a:], the carrier of a:])
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
K38( the carrier of a) is V1() V4( the carrier of a) V5( the carrier of a) V11() V14( the carrier of a) M2( bool [: the carrier of a, the carrier of a:])
K162( the carrier of a, the carrier of a, the multF of a,a,K38( the carrier of a)) is V1() V4( the carrier of a) V5( the carrier of a) Function-like V18( the carrier of a, the carrier of a) M2( bool [: the carrier of a, the carrier of a:])
K174( the carrier of a, the carrier of a,p1,(a multfield)) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
len (a * p1) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
j is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
len j is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
(Line ((1. (a,n)),K)) . K is set
a1 is V21() V22() V23() V27() ext-real non negative set
(Line ((1. (a,n)),K)) . a1 is set
Seg (len (Line ((1. (a,n)),K))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (Line ((1. (a,n)),K)) ) } is set
[K,a1] is set
(Col (A,M2)) . K is set
A * (K,M2) is M2( the carrier of a)
a1 is M2( the carrier of a)
(Col (A,M2)) . l is set
A * (l,M2) is M2( the carrier of a)
a2 is M2( the carrier of a)
[M1,M2] is set
Line ((n,n,a,(1. (a,n)),l,K,a),M1) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width (n,n,a,(1. (a,n)),l,K,a)) FinSequence-like Element of (width (n,n,a,(1. (a,n)),l,K,a)) -tuples_on the carrier of a
(width (n,n,a,(1. (a,n)),l,K,a)) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
(Line ((n,n,a,(1. (a,n)),l,K,a),M1)) "*" (Col (A,M2)) is M2( the carrier of a)
mlt ((Line ((n,n,a,(1. (a,n)),l,K,a),M1)),(Col (A,M2))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,(Line ((n,n,a,(1. (a,n)),l,K,a),M1)),(Col (A,M2))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Sum (mlt ((Line ((n,n,a,(1. (a,n)),l,K,a),M1)),(Col (A,M2)))) is M2( the carrier of a)
(a * p1) + j is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
the addF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) V155( the carrier of a) V156( the carrier of a) M2( bool [:[: the carrier of a, the carrier of a:], the carrier of a:])
K171( the carrier of a, the carrier of a, the carrier of a, the addF of a,(a * p1),j) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
mlt (((a * p1) + j),i) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,((a * p1) + j),i) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Sum (mlt (((a * p1) + j),i)) is M2( the carrier of a)
mlt ((a * p1),i) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,(a * p1),i) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
mlt (j,i) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,j,i) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
(mlt ((a * p1),i)) + (mlt (j,i)) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
K171( the carrier of a, the carrier of a, the carrier of a, the addF of a,(mlt ((a * p1),i)),(mlt (j,i))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Sum ((mlt ((a * p1),i)) + (mlt (j,i))) is M2( the carrier of a)
mlt (p1,i) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,p1,i) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
a * (mlt (p1,i)) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
K174( the carrier of a, the carrier of a,(mlt (p1,i)),(a multfield)) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
(a * (mlt (p1,i))) + (mlt (j,i)) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width A) FinSequence-like Element of (width A) -tuples_on the carrier of a
K171( the carrier of a, the carrier of a, the carrier of a, the addF of a,(a * (mlt (p1,i))),(mlt (j,i))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Sum ((a * (mlt (p1,i))) + (mlt (j,i))) is M2( the carrier of a)
Sum (a * (mlt (p1,i))) is M2( the carrier of a)
Sum (mlt (j,i)) is M2( the carrier of a)
(Sum (a * (mlt (p1,i)))) + (Sum (mlt (j,i))) is M2( the carrier of a)
the addF of a . ((Sum (a * (mlt (p1,i)))),(Sum (mlt (j,i)))) is M2( the carrier of a)
mlt ((Line ((1. (a,n)),K)),(Col (A,M2))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,(Line ((1. (a,n)),K)),(Col (A,M2))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Sum (mlt ((Line ((1. (a,n)),K)),(Col (A,M2)))) is M2( the carrier of a)
a * (Sum (mlt ((Line ((1. (a,n)),K)),(Col (A,M2))))) is M2( the carrier of a)
the multF of a . (a,(Sum (mlt ((Line ((1. (a,n)),K)),(Col (A,M2)))))) is M2( the carrier of a)
mlt ((Line ((1. (a,n)),l)),(Col (A,M2))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,(Line ((1. (a,n)),l)),(Col (A,M2))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Sum (mlt ((Line ((1. (a,n)),l)),(Col (A,M2)))) is M2( the carrier of a)
(a * (Sum (mlt ((Line ((1. (a,n)),K)),(Col (A,M2)))))) + (Sum (mlt ((Line ((1. (a,n)),l)),(Col (A,M2))))) is M2( the carrier of a)
the addF of a . ((a * (Sum (mlt ((Line ((1. (a,n)),K)),(Col (A,M2)))))),(Sum (mlt ((Line ((1. (a,n)),l)),(Col (A,M2)))))) is M2( the carrier of a)
a * a1 is M2( the carrier of a)
the multF of a . (a,a1) is M2( the carrier of a)
(a * a1) + (Sum (mlt ((Line ((1. (a,n)),l)),(Col (A,M2))))) is M2( the carrier of a)
the addF of a . ((a * a1),(Sum (mlt ((Line ((1. (a,n)),l)),(Col (A,M2)))))) is M2( the carrier of a)
(a * a1) + a2 is M2( the carrier of a)
the addF of a . ((a * a1),a2) is M2( the carrier of a)
a * (A * (K,M2)) is M2( the carrier of a)
the multF of a . (a,(A * (K,M2))) is M2( the carrier of a)
(a * (A * (K,M2))) + (A * (l,M2)) is M2( the carrier of a)
the addF of a . ((a * (A * (K,M2))),(A * (l,M2))) is M2( the carrier of a)
M1 is V21() V22() V23() V27() ext-real non negative set
M2 is V21() V22() V23() V27() ext-real non negative set
((n,n,a,(1. (a,n)),l,K,a) * A) * (M1,M2) is M2( the carrier of a)
(n,n,a,A,l,K,a) * (M1,M2) is M2( the carrier of a)
[M1,M1] is set
Line ((1. (a,n)),M1) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width (1. (a,n))) FinSequence-like Element of (width (1. (a,n))) -tuples_on the carrier of a
(width (1. (a,n))) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
(Line ((1. (a,n)),M1)) . M1 is set
1_ a is M2( the carrier of a)
1. a is V47(a) M2( the carrier of a)
dom (Line ((1. (a,n)),M1)) is M2( bool NAT)
0. a is V47(a) M2( the carrier of a)
i is V21() V22() V23() V27() ext-real non negative set
(Line ((1. (a,n)),M1)) . i is set
len (Line ((1. (a,n)),M1)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len (Line ((1. (a,n)),M1))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (Line ((1. (a,n)),M1)) ) } is set
[M1,i] is set
Col (A,M2) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( len A) FinSequence-like Element of (len A) -tuples_on the carrier of a
(len A) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
len (Col (A,M2)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom (Col (A,M2)) is M2( bool NAT)
len (Line ((1. (a,n)),M1)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
[M1,M2] is set
Line ((n,n,a,(1. (a,n)),l,K,a),M1) is V1() V4( NAT ) V5( the carrier of a) Function-like V35( width (n,n,a,(1. (a,n)),l,K,a)) FinSequence-like Element of (width (n,n,a,(1. (a,n)),l,K,a)) -tuples_on the carrier of a
(width (n,n,a,(1. (a,n)),l,K,a)) -tuples_on the carrier of a is functional V11() FinSequence-membered FinSequenceSet of the carrier of a
(Line ((n,n,a,(1. (a,n)),l,K,a),M1)) "*" (Col (A,M2)) is M2( the carrier of a)
mlt ((Line ((n,n,a,(1. (a,n)),l,K,a),M1)),(Col (A,M2))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
the multF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) V155( the carrier of a) M2( bool [:[: the carrier of a, the carrier of a:], the carrier of a:])
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,(Line ((n,n,a,(1. (a,n)),l,K,a),M1)),(Col (A,M2))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Sum (mlt ((Line ((n,n,a,(1. (a,n)),l,K,a),M1)),(Col (A,M2)))) is M2( the carrier of a)
mlt ((Line ((1. (a,n)),M1)),(Col (A,M2))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
K171( the carrier of a, the carrier of a, the carrier of a, the multF of a,(Line ((1. (a,n)),M1)),(Col (A,M2))) is V1() V4( NAT ) V5( the carrier of a) Function-like FinSequence-like FinSequence of the carrier of a
Sum (mlt ((Line ((1. (a,n)),M1)),(Col (A,M2)))) is M2( the carrier of a)
(Col (A,M2)) . M1 is set
A * (M1,M2) is M2( the carrier of a)
M1 is V21() V22() V23() V27() ext-real non negative set
M2 is V21() V22() V23() V27() ext-real non negative set
[M1,M2] is set
((n,n,a,(1. (a,n)),l,K,a) * A) * (M1,M2) is M2( the carrier of a)
(n,n,a,A,l,K,a) * (M1,M2) is M2( the carrier of a)
width (n,n,a,A,l,K,a) is V21() V22() V23() V27() ext-real non negative M2( NAT )
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of a is V11() non trivial set
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
a is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of a
(l,n,a,a,K,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of a
Indices a is set
dom a is M2( bool NAT)
width a is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width a) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width a ) } is set
[:(dom a),(Seg (width a)):] is set
A is V21() V22() V23() V27() ext-real non negative set
M is V21() V22() V23() V27() ext-real non negative set
[A,M] is set
(l,n,a,a,K,K) * (A,M) is M2( the carrier of a)
a * (A,M) is M2( the carrier of a)
a * (K,M) is M2( the carrier of a)
len (l,n,a,a,K,K) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len a is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (l,n,a,a,K,K) is V21() V22() V23() V27() ext-real non negative M2( NAT )
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of a is V11() non trivial set
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
A is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of a
(l,n,a,A,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of a
(l,n,a,A,a,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of a
width (l,n,a,A,a,K) is V21() V22() V23() V27() ext-real non negative M2( NAT )
width A is V21() V22() V23() V27() ext-real non negative M2( NAT )
Indices (l,n,a,A,K,a) is set
dom (l,n,a,A,K,a) is M2( bool NAT)
width (l,n,a,A,K,a) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (l,n,a,A,K,a)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (l,n,a,A,K,a) ) } is set
[:(dom (l,n,a,A,K,a)),(Seg (width (l,n,a,A,K,a))):] is set
M is V21() V22() V23() V27() ext-real non negative set
M1 is V21() V22() V23() V27() ext-real non negative set
[M,M1] is set
(l,n,a,A,K,a) * (M,M1) is M2( the carrier of a)
(l,n,a,A,a,K) * (M,M1) is M2( the carrier of a)
Indices A is set
dom A is M2( bool NAT)
Seg (width A) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width A ) } is set
[:(dom A),(Seg (width A)):] is set
A * (K,M1) is M2( the carrier of a)
A * (a,M1) is M2( the carrier of a)
A * (M,M1) is M2( the carrier of a)
len (l,n,a,A,K,a) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len A is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (l,n,a,A,a,K) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of a is V11() non trivial set
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
A is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of a
dom A is M2( bool NAT)
(l,n,a,A,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of a
(l,n,a,(l,n,a,A,K,a),K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of a
dom (l,n,a,A,K,a) is M2( bool NAT)
len (l,n,a,A,K,a) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len (l,n,a,A,K,a)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (l,n,a,A,K,a) ) } is set
len A is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len A) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len A ) } is set
width (l,n,a,A,K,a) is V21() V22() V23() V27() ext-real non negative M2( NAT )
width A is V21() V22() V23() V27() ext-real non negative M2( NAT )
Indices A is set
Seg (width A) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width A ) } is set
[:(dom A),(Seg (width A)):] is set
M1 is V21() V22() V23() V27() ext-real non negative set
M2 is V21() V22() V23() V27() ext-real non negative set
[M1,M2] is set
(l,n,a,(l,n,a,A,K,a),K,a) * (M1,M2) is M2( the carrier of a)
A * (M1,M2) is M2( the carrier of a)
(l,n,a,A,K,a) * (M1,M2) is M2( the carrier of a)
(l,n,a,(l,n,a,A,K,a),K,a) * (K,M2) is M2( the carrier of a)
(l,n,a,A,K,a) * (a,M2) is M2( the carrier of a)
(l,n,a,(l,n,a,A,K,a),K,a) * (a,M2) is M2( the carrier of a)
(l,n,a,A,K,a) * (K,M2) is M2( the carrier of a)
width (l,n,a,(l,n,a,A,K,a),K,a) is V21() V22() V23() V27() ext-real non negative M2( NAT )
len (l,n,a,(l,n,a,A,K,a),K,a) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
1. (a,n) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
the carrier of a is V11() non trivial set
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
dom (1. (a,n)) is M2( bool NAT)
(n,n,a,(1. (a,n)),l,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K) ~ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K) * (n,n,a,(1. (a,n)),l,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(n,n,a,(1. (a,n)),l,K),l,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
l is V21() V22() V23() V27() ext-real non negative set
n is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of n is V11() non trivial set
1. (n,l) is V1() V4( NAT ) V5( the carrier of n * ) Function-like FinSequence-like tabular Matrix of l,l, the carrier of n
the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n
Indices (1. (n,l)) is set
dom (1. (n,l)) is M2( bool NAT)
width (1. (n,l)) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (1. (n,l))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (1. (n,l)) ) } is set
[:(dom (1. (n,l))),(Seg (width (1. (n,l)))):] is set
K is V21() V22() V23() V27() ext-real non negative set
a is V21() V22() V23() V27() ext-real non negative set
[K,a] is set
(1. (n,l)) * (K,a) is M2( the carrier of n)
a is V21() V22() V23() V27() ext-real non negative set
A is V21() V22() V23() V27() ext-real non negative set
M is M2( the carrier of n)
- M is M2( the carrier of n)
(l,l,n,(1. (n,l)),a,A,(- M)) is V1() V4( NAT ) V5( the carrier of n * ) Function-like FinSequence-like tabular Matrix of l,l, the carrier of n
(l,l,n,(l,l,n,(1. (n,l)),a,A,(- M)),a,A,M) is V1() V4( NAT ) V5( the carrier of n * ) Function-like FinSequence-like tabular Matrix of l,l, the carrier of n
(l,l,n,(l,l,n,(1. (n,l)),a,A,(- M)),a,A,M) * (K,a) is M2( the carrier of n)
width (l,l,n,(1. (n,l)),a,A,(- M)) is V21() V22() V23() V27() ext-real non negative M2( NAT )
width (l,l,n,(l,l,n,(1. (n,l)),a,A,(- M)),a,A,M) is V21() V22() V23() V27() ext-real non negative M2( NAT )
dom (l,l,n,(1. (n,l)),a,A,(- M)) is M2( bool NAT)
len (l,l,n,(1. (n,l)),a,A,(- M)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len (l,l,n,(1. (n,l)),a,A,(- M))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (l,l,n,(1. (n,l)),a,A,(- M)) ) } is set
len (1. (n,l)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len (1. (n,l))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (1. (n,l)) ) } is set
(width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n is functional V11() FinSequence-membered FinSequenceSet of the carrier of n
Line ((1. (n,l)),K) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (1. (n,l))) FinSequence-like Element of (width (1. (n,l))) -tuples_on the carrier of n
(width (1. (n,l))) -tuples_on the carrier of n is functional V11() FinSequence-membered FinSequenceSet of the carrier of n
Line ((1. (n,l)),A) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (1. (n,l))) FinSequence-like Element of (width (1. (n,l))) -tuples_on the carrier of n
Line ((l,l,n,(1. (n,l)),a,A,(- M)),A) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
Line ((l,l,n,(l,l,n,(1. (n,l)),a,A,(- M)),a,A,M),K) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(l,l,n,(1. (n,l)),a,A,(- M)),a,A,M)) FinSequence-like Element of (width (l,l,n,(l,l,n,(1. (n,l)),a,A,(- M)),a,A,M)) -tuples_on the carrier of n
(width (l,l,n,(l,l,n,(1. (n,l)),a,A,(- M)),a,A,M)) -tuples_on the carrier of n is functional V11() FinSequence-membered FinSequenceSet of the carrier of n
M * (Line ((l,l,n,(1. (n,l)),a,A,(- M)),A)) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
M multfield is V1() V4( the carrier of n) V5( the carrier of n) Function-like V18( the carrier of n, the carrier of n) M2( bool [: the carrier of n, the carrier of n:])
[: the carrier of n, the carrier of n:] is set
bool [: the carrier of n, the carrier of n:] is set
the multF of n is V1() V4([: the carrier of n, the carrier of n:]) V5( the carrier of n) Function-like V18([: the carrier of n, the carrier of n:], the carrier of n) V155( the carrier of n) M2( bool [:[: the carrier of n, the carrier of n:], the carrier of n:])
[:[: the carrier of n, the carrier of n:], the carrier of n:] is set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set
K38( the carrier of n) is V1() V4( the carrier of n) V5( the carrier of n) V11() V14( the carrier of n) M2( bool [: the carrier of n, the carrier of n:])
K162( the carrier of n, the carrier of n, the multF of n,M,K38( the carrier of n)) is V1() V4( the carrier of n) V5( the carrier of n) Function-like V18( the carrier of n, the carrier of n) M2( bool [: the carrier of n, the carrier of n:])
K174( the carrier of n, the carrier of n,(Line ((l,l,n,(1. (n,l)),a,A,(- M)),A)),(M multfield)) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
Line ((l,l,n,(1. (n,l)),a,A,(- M)),K) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
(M * (Line ((l,l,n,(1. (n,l)),a,A,(- M)),A))) + (Line ((l,l,n,(1. (n,l)),a,A,(- M)),K)) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
the addF of n is V1() V4([: the carrier of n, the carrier of n:]) V5( the carrier of n) Function-like V18([: the carrier of n, the carrier of n:], the carrier of n) V155( the carrier of n) V156( the carrier of n) M2( bool [:[: the carrier of n, the carrier of n:], the carrier of n:])
K171( the carrier of n, the carrier of n, the carrier of n, the addF of n,(M * (Line ((l,l,n,(1. (n,l)),a,A,(- M)),A))),(Line ((l,l,n,(1. (n,l)),a,A,(- M)),K))) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
i is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
M * i is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
K174( the carrier of n, the carrier of n,i,(M multfield)) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
(- M) * i is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
(- M) multfield is V1() V4( the carrier of n) V5( the carrier of n) Function-like V18( the carrier of n, the carrier of n) M2( bool [: the carrier of n, the carrier of n:])
K162( the carrier of n, the carrier of n, the multF of n,(- M),K38( the carrier of n)) is V1() V4( the carrier of n) V5( the carrier of n) Function-like V18( the carrier of n, the carrier of n) M2( bool [: the carrier of n, the carrier of n:])
K174( the carrier of n, the carrier of n,i,((- M) multfield)) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
M2 is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
((- M) * i) + M2 is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
K171( the carrier of n, the carrier of n, the carrier of n, the addF of n,((- M) * i),M2) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
(M * i) + (((- M) * i) + M2) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
K171( the carrier of n, the carrier of n, the carrier of n, the addF of n,(M * i),(((- M) * i) + M2)) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
(M * i) + ((- M) * i) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
K171( the carrier of n, the carrier of n, the carrier of n, the addF of n,(M * i),((- M) * i)) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
((M * i) + ((- M) * i)) + M2 is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
K171( the carrier of n, the carrier of n, the carrier of n, the addF of n,((M * i) + ((- M) * i)),M2) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
M + (- M) is M2( the carrier of n)
the addF of n . (M,(- M)) is M2( the carrier of n)
(M + (- M)) * i is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
(M + (- M)) multfield is V1() V4( the carrier of n) V5( the carrier of n) Function-like V18( the carrier of n, the carrier of n) M2( bool [: the carrier of n, the carrier of n:])
K162( the carrier of n, the carrier of n, the multF of n,(M + (- M)),K38( the carrier of n)) is V1() V4( the carrier of n) V5( the carrier of n) Function-like V18( the carrier of n, the carrier of n) M2( bool [: the carrier of n, the carrier of n:])
K174( the carrier of n, the carrier of n,i,((M + (- M)) multfield)) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
((M + (- M)) * i) + M2 is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
K171( the carrier of n, the carrier of n, the carrier of n, the addF of n,((M + (- M)) * i),M2) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
0. n is V47(n) M2( the carrier of n)
(0. n) * i is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
(0. n) multfield is V1() V4( the carrier of n) V5( the carrier of n) Function-like V18( the carrier of n, the carrier of n) M2( bool [: the carrier of n, the carrier of n:])
K162( the carrier of n, the carrier of n, the multF of n,(0. n),K38( the carrier of n)) is V1() V4( the carrier of n) V5( the carrier of n) Function-like V18( the carrier of n, the carrier of n) M2( bool [: the carrier of n, the carrier of n:])
K174( the carrier of n, the carrier of n,i,((0. n) multfield)) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
((0. n) * i) + M2 is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
K171( the carrier of n, the carrier of n, the carrier of n, the addF of n,((0. n) * i),M2) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
(width (l,l,n,(1. (n,l)),a,A,(- M))) |-> (0. n) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
((width (l,l,n,(1. (n,l)),a,A,(- M))) |-> (0. n)) + M2 is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
K171( the carrier of n, the carrier of n, the carrier of n, the addF of n,((width (l,l,n,(1. (n,l)),a,A,(- M))) |-> (0. n)),M2) is V1() V4( NAT ) V5( the carrier of n) Function-like FinSequence-like FinSequence of the carrier of n
(Line ((1. (n,l)),K)) . a is set
Line ((l,l,n,(l,l,n,(1. (n,l)),a,A,(- M)),a,A,M),K) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(l,l,n,(1. (n,l)),a,A,(- M)),a,A,M)) FinSequence-like Element of (width (l,l,n,(l,l,n,(1. (n,l)),a,A,(- M)),a,A,M)) -tuples_on the carrier of n
(width (l,l,n,(l,l,n,(1. (n,l)),a,A,(- M)),a,A,M)) -tuples_on the carrier of n is functional V11() FinSequence-membered FinSequenceSet of the carrier of n
Line ((l,l,n,(1. (n,l)),a,A,(- M)),K) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (l,l,n,(1. (n,l)),a,A,(- M))) FinSequence-like Element of (width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n
(width (l,l,n,(1. (n,l)),a,A,(- M))) -tuples_on the carrier of n is functional V11() FinSequence-membered FinSequenceSet of the carrier of n
(Line ((l,l,n,(l,l,n,(1. (n,l)),a,A,(- M)),a,A,M),K)) . a is set
Line ((1. (n,l)),K) is V1() V4( NAT ) V5( the carrier of n) Function-like V35( width (1. (n,l))) FinSequence-like Element of (width (1. (n,l))) -tuples_on the carrier of n
(width (1. (n,l))) -tuples_on the carrier of n is functional V11() FinSequence-membered FinSequenceSet of the carrier of n
(Line ((1. (n,l)),K)) . a is set
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of a is V11() non trivial set
1. (a,n) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
dom (1. (a,n)) is M2( bool NAT)
a is M2( the carrier of a)
(n,n,a,(1. (a,n)),l,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K,a) ~ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
- a is M2( the carrier of a)
(n,n,a,(1. (a,n)),l,K,(- a)) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
Indices (1. (a,n)) is set
width (1. (a,n)) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (1. (a,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (1. (a,n)) ) } is set
[:(dom (1. (a,n))),(Seg (width (1. (a,n)))):] is set
(n,n,a,(n,n,a,(1. (a,n)),l,K,(- a)),l,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
M is V21() V22() V23() V27() ext-real non negative set
M1 is V21() V22() V23() V27() ext-real non negative set
[M,M1] is set
(1. (a,n)) * (M,M1) is M2( the carrier of a)
(n,n,a,(n,n,a,(1. (a,n)),l,K,(- a)),l,K,a) * (M,M1) is M2( the carrier of a)
a + (- a) is M2( the carrier of a)
the addF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) V155( the carrier of a) V156( the carrier of a) M2( bool [:[: the carrier of a, the carrier of a:], the carrier of a:])
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the addF of a . (a,(- a)) is M2( the carrier of a)
0. a is V47(a) M2( the carrier of a)
- (- a) is M2( the carrier of a)
(n,n,a,(n,n,a,(1. (a,n)),l,K,a),l,K,(- a)) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
M2 is V21() V22() V23() V27() ext-real non negative set
i is V21() V22() V23() V27() ext-real non negative set
[M2,i] is set
(1. (a,n)) * (M2,i) is M2( the carrier of a)
(n,n,a,(n,n,a,(1. (a,n)),l,K,a),l,K,(- a)) * (M2,i) is M2( the carrier of a)
(n,n,a,(1. (a,n)),l,K,a) * (n,n,a,(1. (a,n)),l,K,(- a)) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K,(- a)) * (n,n,a,(1. (a,n)),l,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
1. (K,n) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
dom (1. (K,n)) is M2( bool NAT)
0. K is V47(K) M2( the carrier of K)
a is M2( the carrier of K)
(n,n,K,(1. (K,n)),l,a) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,(1. (K,n)),l,a) ~ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
a " is M2( the carrier of K)
(n,n,K,(1. (K,n)),l,(a ")) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
dom (n,n,K,(1. (K,n)),l,a) is M2( bool NAT)
len (n,n,K,(1. (K,n)),l,a) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len (n,n,K,(1. (K,n)),l,a)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (n,n,K,(1. (K,n)),l,a) ) } is set
len (1. (K,n)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len (1. (K,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (1. (K,n)) ) } is set
dom (n,n,K,(1. (K,n)),l,(a ")) is M2( bool NAT)
len (n,n,K,(1. (K,n)),l,(a ")) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len (n,n,K,(1. (K,n)),l,(a "))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (n,n,K,(1. (K,n)),l,(a ")) ) } is set
width (n,n,K,(1. (K,n)),l,(a ")) is V21() V22() V23() V27() ext-real non negative M2( NAT )
width (1. (K,n)) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Indices (1. (K,n)) is set
Seg (width (1. (K,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (1. (K,n)) ) } is set
[:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] is set
(n,n,K,(n,n,K,(1. (K,n)),l,(a ")),l,a) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
M is V21() V22() V23() V27() ext-real non negative set
M1 is V21() V22() V23() V27() ext-real non negative set
[M,M1] is set
(1. (K,n)) * (M,M1) is M2( the carrier of K)
(n,n,K,(n,n,K,(1. (K,n)),l,(a ")),l,a) * (M,M1) is M2( the carrier of K)
(n,n,K,(1. (K,n)),l,(a ")) * (M,M1) is M2( the carrier of K)
(n,n,K,(1. (K,n)),l,(a ")) * (l,M1) is M2( the carrier of K)
(1. (K,n)) * (l,M1) is M2( the carrier of K)
(a ") * ((1. (K,n)) * (l,M1)) is M2( the carrier of K)
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
[: the carrier of K, the carrier of K:] is set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the multF of K . ((a "),((1. (K,n)) * (l,M1))) is M2( the carrier of K)
(n,n,K,(n,n,K,(1. (K,n)),l,(a ")),l,a) * (l,M1) is M2( the carrier of K)
a * ((a ") * ((1. (K,n)) * (l,M1))) is M2( the carrier of K)
the multF of K . (a,((a ") * ((1. (K,n)) * (l,M1)))) is M2( the carrier of K)
a * (a ") is M2( the carrier of K)
the multF of K . (a,(a ")) is M2( the carrier of K)
(a * (a ")) * ((1. (K,n)) * (l,M1)) is M2( the carrier of K)
the multF of K . ((a * (a ")),((1. (K,n)) * (l,M1))) is M2( the carrier of K)
1_ K is M2( the carrier of K)
1. K is V47(K) M2( the carrier of K)
(1_ K) * ((1. (K,n)) * (l,M1)) is M2( the carrier of K)
the multF of K . ((1_ K),((1. (K,n)) * (l,M1))) is M2( the carrier of K)
width (n,n,K,(1. (K,n)),l,a) is V21() V22() V23() V27() ext-real non negative M2( NAT )
(n,n,K,(n,n,K,(1. (K,n)),l,a),l,(a ")) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
M is V21() V22() V23() V27() ext-real non negative set
M1 is V21() V22() V23() V27() ext-real non negative set
[M,M1] is set
(1. (K,n)) * (M,M1) is M2( the carrier of K)
(n,n,K,(n,n,K,(1. (K,n)),l,a),l,(a ")) * (M,M1) is M2( the carrier of K)
(n,n,K,(1. (K,n)),l,a) * (M,M1) is M2( the carrier of K)
(n,n,K,(1. (K,n)),l,a) * (l,M1) is M2( the carrier of K)
(1. (K,n)) * (l,M1) is M2( the carrier of K)
a * ((1. (K,n)) * (l,M1)) is M2( the carrier of K)
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
[: the carrier of K, the carrier of K:] is set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the multF of K . (a,((1. (K,n)) * (l,M1))) is M2( the carrier of K)
(n,n,K,(n,n,K,(1. (K,n)),l,a),l,(a ")) * (l,M1) is M2( the carrier of K)
(a ") * (a * ((1. (K,n)) * (l,M1))) is M2( the carrier of K)
the multF of K . ((a "),(a * ((1. (K,n)) * (l,M1)))) is M2( the carrier of K)
(a ") * a is M2( the carrier of K)
the multF of K . ((a "),a) is M2( the carrier of K)
((a ") * a) * ((1. (K,n)) * (l,M1)) is M2( the carrier of K)
the multF of K . (((a ") * a),((1. (K,n)) * (l,M1))) is M2( the carrier of K)
1_ K is M2( the carrier of K)
1. K is V47(K) M2( the carrier of K)
(1_ K) * ((1. (K,n)) * (l,M1)) is M2( the carrier of K)
the multF of K . ((1_ K),((1. (K,n)) * (l,M1))) is M2( the carrier of K)
(n,n,K,(1. (K,n)),l,a) * (n,n,K,(1. (K,n)),l,(a ")) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,(1. (K,n)),l,(a ")) * (n,n,K,(1. (K,n)),l,a) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
a is V21() V22() V23() V27() ext-real non negative set
a is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
width a is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width a) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width a ) } is set
A is V21() V22() V23() V27() ext-real non negative set
len a is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom a is M2( bool NAT)
a @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (a @) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (a @) is V21() V22() V23() V27() ext-real non negative M2( NAT )
M is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
(n,l,K,M,a,A) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
width (n,l,K,M,a,A) is V21() V22() V23() V27() ext-real non negative M2( NAT )
(n,l,K,M,a,A) @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular FinSequence of the carrier of K *
len ((n,l,K,M,a,A) @) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (n,l,K,M,a,A) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width ((n,l,K,M,a,A) @) is V21() V22() V23() V27() ext-real non negative M2( NAT )
M1 is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
M2 is V21() V22() V23() V27() ext-real non negative set
a * (M2,A) is M2( the carrier of K)
a * (M2,a) is M2( the carrier of K)
i is V21() V22() V23() V27() ext-real non negative set
M1 * (M2,i) is M2( the carrier of K)
a * (M2,i) is M2( the carrier of K)
[M2,i] is set
Indices a is set
[:(dom a),(Seg (width a)):] is set
[i,M2] is set
Indices M is set
dom M is M2( bool NAT)
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
dom (n,l,K,M,a,A) is M2( bool NAT)
Seg (len (n,l,K,M,a,A)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (n,l,K,M,a,A) ) } is set
len M is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len M ) } is set
Indices (n,l,K,M,a,A) is set
Seg (width (n,l,K,M,a,A)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (n,l,K,M,a,A) ) } is set
[:(dom (n,l,K,M,a,A)),(Seg (width (n,l,K,M,a,A))):] is set
[M2,A] is set
(n,l,K,M,a,A) * (i,M2) is M2( the carrier of K)
M * (A,M2) is M2( the carrier of K)
[M2,a] is set
(n,l,K,M,a,A) * (i,M2) is M2( the carrier of K)
M * (a,M2) is M2( the carrier of K)
(n,l,K,M,a,A) * (i,M2) is M2( the carrier of K)
M * (i,M2) is M2( the carrier of K)
M2 is V21() V22() V23() V27() ext-real non negative set
i is V21() V22() V23() V27() ext-real non negative set
M1 * (M2,i) is M2( the carrier of K)
a * (M2,A) is M2( the carrier of K)
a * (M2,a) is M2( the carrier of K)
a * (M2,i) is M2( the carrier of K)
M is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
M1 is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Indices M is set
dom M is M2( bool NAT)
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Indices a is set
[:(dom a),(Seg (width a)):] is set
M2 is V21() V22() V23() V27() ext-real non negative set
i is V21() V22() V23() V27() ext-real non negative set
[M2,i] is set
M * (M2,i) is M2( the carrier of K)
M1 * (M2,i) is M2( the carrier of K)
a * (M2,a) is M2( the carrier of K)
a * (M2,A) is M2( the carrier of K)
a * (M2,i) is M2( the carrier of K)
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
a is V21() V22() V23() V27() ext-real non negative set
a is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
width a is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width a) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width a ) } is set
len a is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom a is M2( bool NAT)
A is M2( the carrier of K)
a @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (a @) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (a @) is V21() V22() V23() V27() ext-real non negative M2( NAT )
M is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
(n,l,K,M,a,A) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
width (n,l,K,M,a,A) is V21() V22() V23() V27() ext-real non negative M2( NAT )
(n,l,K,M,a,A) @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular FinSequence of the carrier of K *
len ((n,l,K,M,a,A) @) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (n,l,K,M,a,A) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width ((n,l,K,M,a,A) @) is V21() V22() V23() V27() ext-real non negative M2( NAT )
M1 is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
M2 is V21() V22() V23() V27() ext-real non negative set
a * (M2,a) is M2( the carrier of K)
A * (a * (M2,a)) is M2( the carrier of K)
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
[: the carrier of K, the carrier of K:] is set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the multF of K . (A,(a * (M2,a))) is M2( the carrier of K)
i is V21() V22() V23() V27() ext-real non negative set
M1 * (M2,i) is M2( the carrier of K)
a * (M2,i) is M2( the carrier of K)
[M2,i] is set
Indices a is set
[:(dom a),(Seg (width a)):] is set
[i,M2] is set
Indices M is set
dom M is M2( bool NAT)
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
dom (n,l,K,M,a,A) is M2( bool NAT)
Seg (len (n,l,K,M,a,A)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (n,l,K,M,a,A) ) } is set
len M is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Seg (len M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len M ) } is set
Indices (n,l,K,M,a,A) is set
Seg (width (n,l,K,M,a,A)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (n,l,K,M,a,A) ) } is set
[:(dom (n,l,K,M,a,A)),(Seg (width (n,l,K,M,a,A))):] is set
[M2,a] is set
(n,l,K,M,a,A) * (i,M2) is M2( the carrier of K)
M * (a,M2) is M2( the carrier of K)
A * (M * (a,M2)) is M2( the carrier of K)
the multF of K . (A,(M * (a,M2))) is M2( the carrier of K)
(n,l,K,M,a,A) * (i,M2) is M2( the carrier of K)
M * (i,M2) is M2( the carrier of K)
M2 is V21() V22() V23() V27() ext-real non negative set
i is V21() V22() V23() V27() ext-real non negative set
M1 * (M2,i) is M2( the carrier of K)
a * (M2,a) is M2( the carrier of K)
A * (a * (M2,a)) is M2( the carrier of K)
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
[: the carrier of K, the carrier of K:] is set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the multF of K . (A,(a * (M2,a))) is M2( the carrier of K)
a * (M2,i) is M2( the carrier of K)
M is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
M1 is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Indices M is set
dom M is M2( bool NAT)
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Indices a is set
[:(dom a),(Seg (width a)):] is set
M2 is V21() V22() V23() V27() ext-real non negative set
i is V21() V22() V23() V27() ext-real non negative set
[M2,i] is set
M * (M2,i) is M2( the carrier of K)
M1 * (M2,i) is M2( the carrier of K)
a * (M2,i) is M2( the carrier of K)
a * (M2,a) is M2( the carrier of K)
A * (a * (M2,a)) is M2( the carrier of K)
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
[: the carrier of K, the carrier of K:] is set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the multF of K . (A,(a * (M2,a))) is M2( the carrier of K)
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
a is V21() V22() V23() V27() ext-real non negative set
a is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
width a is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width a) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width a ) } is set
A is V21() V22() V23() V27() ext-real non negative set
len a is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom a is M2( bool NAT)
M is M2( the carrier of K)
a @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (a @) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (a @) is V21() V22() V23() V27() ext-real non negative M2( NAT )
M1 is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
(n,l,K,M1,a,A,M) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,l, the carrier of K
width (n,l,K,M1,a,A,M) is V21() V22() V23() V27() ext-real non negative M2( NAT )
(n,l,K,M1,a,A,M) @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular FinSequence of the carrier of K *
len ((n,l,K,M1,a,A,M) @) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (n,l,K,M1,a,A,M) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width ((n,l,K,M1,a,A,M) @) is V21() V22() V23() V27() ext-real non negative M2( NAT )
M2 is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M2 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
i is V21() V22() V23() V27() ext-real non negative set
a * (i,A) is M2( the carrier of K)
M * (a * (i,A)) is M2( the carrier of K)
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
[: the carrier of K, the carrier of K:] is set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the multF of K . (M,(a * (i,A))) is M2( the carrier of K)
a * (i,a) is M2( the carrier of K)
(M * (a * (i,A))) + (a * (i,a)) is M2( the carrier of K)
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) V156( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
the addF of K . ((M * (a * (i,A))),(a * (i,a))) is M2( the carrier of K)
j is V21() V22() V23() V27() ext-real non negative set
M2 * (i,j) is M2( the carrier of K)
a * (i,j) is M2( the carrier of K)
[i,j] is set
Indices a is set
[:(dom a),(Seg (width a)):] is set
[j,i] is set
Indices M1 is set
dom M1 is M2( bool NAT)
width M1 is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width M1) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M1 ) } is set
[:(dom M1),(Seg (width M1)):] is set
len M1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom (n,l,K,M1,a,A,M) is M2( bool NAT)
Seg (len (n,l,K,M1,a,A,M)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (n,l,K,M1,a,A,M) ) } is set
Seg (len M1) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len M1 ) } is set
Indices (n,l,K,M1,a,A,M) is set
Seg (width (n,l,K,M1,a,A,M)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (n,l,K,M1,a,A,M) ) } is set
[:(dom (n,l,K,M1,a,A,M)),(Seg (width (n,l,K,M1,a,A,M))):] is set
[i,A] is set
[i,a] is set
(n,l,K,M1,a,A,M) * (j,i) is M2( the carrier of K)
M1 * (A,i) is M2( the carrier of K)
M * (M1 * (A,i)) is M2( the carrier of K)
the multF of K . (M,(M1 * (A,i))) is M2( the carrier of K)
M1 * (a,i) is M2( the carrier of K)
(M * (M1 * (A,i))) + (M1 * (a,i)) is M2( the carrier of K)
the addF of K . ((M * (M1 * (A,i))),(M1 * (a,i))) is M2( the carrier of K)
(M * (a * (i,A))) + (M1 * (a,i)) is M2( the carrier of K)
the addF of K . ((M * (a * (i,A))),(M1 * (a,i))) is M2( the carrier of K)
(n,l,K,M1,a,A,M) * (j,i) is M2( the carrier of K)
M1 * (j,i) is M2( the carrier of K)
i is V21() V22() V23() V27() ext-real non negative set
j is V21() V22() V23() V27() ext-real non negative set
M2 * (i,j) is M2( the carrier of K)
a * (i,A) is M2( the carrier of K)
M * (a * (i,A)) is M2( the carrier of K)
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
[: the carrier of K, the carrier of K:] is set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the multF of K . (M,(a * (i,A))) is M2( the carrier of K)
a * (i,a) is M2( the carrier of K)
(M * (a * (i,A))) + (a * (i,a)) is M2( the carrier of K)
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) V156( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
the addF of K . ((M * (a * (i,A))),(a * (i,a))) is M2( the carrier of K)
a * (i,j) is M2( the carrier of K)
M1 is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
M2 is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of l,n, the carrier of K
len M2 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
Indices M1 is set
dom M1 is M2( bool NAT)
width M1 is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width M1) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M1 ) } is set
[:(dom M1),(Seg (width M1)):] is set
Indices a is set
[:(dom a),(Seg (width a)):] is set
i is V21() V22() V23() V27() ext-real non negative set
j is V21() V22() V23() V27() ext-real non negative set
[i,j] is set
M1 * (i,j) is M2( the carrier of K)
M2 * (i,j) is M2( the carrier of K)
a * (i,j) is M2( the carrier of K)
a * (i,A) is M2( the carrier of K)
M * (a * (i,A)) is M2( the carrier of K)
the multF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
[: the carrier of K, the carrier of K:] is set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the multF of K . (M,(a * (i,A))) is M2( the carrier of K)
a * (i,a) is M2( the carrier of K)
(M * (a * (i,A))) + (a * (i,a)) is M2( the carrier of K)
the addF of K is V1() V4([: the carrier of K, the carrier of K:]) V5( the carrier of K) Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) V155( the carrier of K) V156( the carrier of K) M2( bool [:[: the carrier of K, the carrier of K:], the carrier of K:])
the addF of K . ((M * (a * (i,A))),(a * (i,a))) is M2( the carrier of K)
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of a is V11() non trivial set
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
A is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of K,a, the carrier of a
width A is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width A) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width A ) } is set
A @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular FinSequence of the carrier of a *
(K,a,a,A,l,n) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of K,a, the carrier of a
M is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of K,a, the carrier of a
(K,a,a,M,l,n) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of K,a, the carrier of a
(K,a,a,M,l,n) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular FinSequence of the carrier of a *
width (K,a,a,M,l,n) is V21() V22() V23() V27() ext-real non negative M2( NAT )
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
len A is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len ((K,a,a,M,l,n) @) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (K,a,a,M,l,n) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len M is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width ((K,a,a,M,l,n) @) is V21() V22() V23() V27() ext-real non negative M2( NAT )
M1 is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of K,a, the carrier of a
dom A is M2( bool NAT)
M2 is V21() V22() V23() V27() ext-real non negative set
A * (M2,n) is M2( the carrier of a)
A * (M2,l) is M2( the carrier of a)
i is V21() V22() V23() V27() ext-real non negative set
M1 * (M2,i) is M2( the carrier of a)
A * (M2,i) is M2( the carrier of a)
[M2,i] is set
Indices A is set
[:(dom A),(Seg (width A)):] is set
[i,M2] is set
Indices M is set
dom M is M2( bool NAT)
Seg (width M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
dom (K,a,a,M,l,n) is M2( bool NAT)
Seg (len (K,a,a,M,l,n)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (K,a,a,M,l,n) ) } is set
Seg (len M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len M ) } is set
Indices (K,a,a,M,l,n) is set
Seg (width (K,a,a,M,l,n)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (K,a,a,M,l,n) ) } is set
[:(dom (K,a,a,M,l,n)),(Seg (width (K,a,a,M,l,n))):] is set
[M2,n] is set
(K,a,a,M,l,n) * (i,M2) is M2( the carrier of a)
M * (n,M2) is M2( the carrier of a)
[M2,l] is set
(K,a,a,M,l,n) * (i,M2) is M2( the carrier of a)
M * (l,M2) is M2( the carrier of a)
(K,a,a,M,l,n) * (i,M2) is M2( the carrier of a)
M * (i,M2) is M2( the carrier of a)
Indices (K,a,a,A,l,n) is set
dom (K,a,a,A,l,n) is M2( bool NAT)
width (K,a,a,A,l,n) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (K,a,a,A,l,n)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (K,a,a,A,l,n) ) } is set
[:(dom (K,a,a,A,l,n)),(Seg (width (K,a,a,A,l,n))):] is set
Indices A is set
[:(dom A),(Seg (width A)):] is set
M2 is V21() V22() V23() V27() ext-real non negative set
i is V21() V22() V23() V27() ext-real non negative set
[M2,i] is set
(K,a,a,A,l,n) * (M2,i) is M2( the carrier of a)
((K,a,a,M,l,n) @) * (M2,i) is M2( the carrier of a)
A * (M2,n) is M2( the carrier of a)
A * (M2,l) is M2( the carrier of a)
A * (M2,i) is M2( the carrier of a)
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of a is V11() non trivial set
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
a is M2( the carrier of a)
A is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,K, the carrier of a
width A is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width A) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width A ) } is set
A @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular FinSequence of the carrier of a *
(n,K,a,A,l,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,K, the carrier of a
M is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,K, the carrier of a
(n,K,a,M,l,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,K, the carrier of a
(n,K,a,M,l,a) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular FinSequence of the carrier of a *
width (n,K,a,M,l,a) is V21() V22() V23() V27() ext-real non negative M2( NAT )
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
len A is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len ((n,K,a,M,l,a) @) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len (n,K,a,M,l,a) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len M is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width ((n,K,a,M,l,a) @) is V21() V22() V23() V27() ext-real non negative M2( NAT )
M1 is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,K, the carrier of a
dom A is M2( bool NAT)
M2 is V21() V22() V23() V27() ext-real non negative set
A * (M2,l) is M2( the carrier of a)
a * (A * (M2,l)) is M2( the carrier of a)
the multF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) V155( the carrier of a) M2( bool [:[: the carrier of a, the carrier of a:], the carrier of a:])
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the multF of a . (a,(A * (M2,l))) is M2( the carrier of a)
i is V21() V22() V23() V27() ext-real non negative set
M1 * (M2,i) is M2( the carrier of a)
A * (M2,i) is M2( the carrier of a)
[M2,i] is set
Indices A is set
[:(dom A),(Seg (width A)):] is set
[i,M2] is set
Indices M is set
dom M is M2( bool NAT)
Seg (width M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
dom (n,K,a,M,l,a) is M2( bool NAT)
Seg (len (n,K,a,M,l,a)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (n,K,a,M,l,a) ) } is set
Seg (len M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len M ) } is set
Indices (n,K,a,M,l,a) is set
Seg (width (n,K,a,M,l,a)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (n,K,a,M,l,a) ) } is set
[:(dom (n,K,a,M,l,a)),(Seg (width (n,K,a,M,l,a))):] is set
(n,K,a,M,l,a) * (i,M2) is M2( the carrier of a)
M * (l,M2) is M2( the carrier of a)
a * (M * (l,M2)) is M2( the carrier of a)
the multF of a . (a,(M * (l,M2))) is M2( the carrier of a)
(n,K,a,M,l,a) * (i,M2) is M2( the carrier of a)
M * (i,M2) is M2( the carrier of a)
Indices (n,K,a,A,l,a) is set
dom (n,K,a,A,l,a) is M2( bool NAT)
width (n,K,a,A,l,a) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (n,K,a,A,l,a)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (n,K,a,A,l,a) ) } is set
[:(dom (n,K,a,A,l,a)),(Seg (width (n,K,a,A,l,a))):] is set
Indices A is set
[:(dom A),(Seg (width A)):] is set
M2 is V21() V22() V23() V27() ext-real non negative set
i is V21() V22() V23() V27() ext-real non negative set
[M2,i] is set
(n,K,a,A,l,a) * (M2,i) is M2( the carrier of a)
((n,K,a,M,l,a) @) * (M2,i) is M2( the carrier of a)
A * (M2,l) is M2( the carrier of a)
a * (A * (M2,l)) is M2( the carrier of a)
the multF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) V155( the carrier of a) M2( bool [:[: the carrier of a, the carrier of a:], the carrier of a:])
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the multF of a . (a,(A * (M2,l))) is M2( the carrier of a)
A * (M2,i) is M2( the carrier of a)
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of a is V11() non trivial set
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
A is M2( the carrier of a)
M is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of K,a, the carrier of a
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width M) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M ) } is set
M @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular FinSequence of the carrier of a *
(K,a,a,M,l,n,A) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of K,a, the carrier of a
M1 is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of K,a, the carrier of a
(K,a,a,M1,l,n,A) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of K,a, the carrier of a
(K,a,a,M1,l,n,A) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular FinSequence of the carrier of a *
len M1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (K,a,a,M1,l,n,A) is V21() V22() V23() V27() ext-real non negative M2( NAT )
width M1 is V21() V22() V23() V27() ext-real non negative M2( NAT )
len M is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len ((K,a,a,M1,l,n,A) @) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
dom M1 is M2( bool NAT)
Seg (len M1) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len M1 ) } is set
len (K,a,a,M1,l,n,A) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width ((K,a,a,M1,l,n,A) @) is V21() V22() V23() V27() ext-real non negative M2( NAT )
M2 is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of K,a, the carrier of a
dom M is M2( bool NAT)
i is V21() V22() V23() V27() ext-real non negative set
M * (i,n) is M2( the carrier of a)
A * (M * (i,n)) is M2( the carrier of a)
the multF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) V155( the carrier of a) M2( bool [:[: the carrier of a, the carrier of a:], the carrier of a:])
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the multF of a . (A,(M * (i,n))) is M2( the carrier of a)
M * (i,l) is M2( the carrier of a)
(A * (M * (i,n))) + (M * (i,l)) is M2( the carrier of a)
the addF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) V155( the carrier of a) V156( the carrier of a) M2( bool [:[: the carrier of a, the carrier of a:], the carrier of a:])
the addF of a . ((A * (M * (i,n))),(M * (i,l))) is M2( the carrier of a)
j is V21() V22() V23() V27() ext-real non negative set
M2 * (i,j) is M2( the carrier of a)
M * (i,j) is M2( the carrier of a)
[i,j] is set
Indices M is set
[:(dom M),(Seg (width M)):] is set
[j,i] is set
Indices M1 is set
Seg (width M1) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width M1 ) } is set
[:(dom M1),(Seg (width M1)):] is set
dom (K,a,a,M1,l,n,A) is M2( bool NAT)
Seg (len (K,a,a,M1,l,n,A)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= len (K,a,a,M1,l,n,A) ) } is set
Indices (K,a,a,M1,l,n,A) is set
Seg (width (K,a,a,M1,l,n,A)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (K,a,a,M1,l,n,A) ) } is set
[:(dom (K,a,a,M1,l,n,A)),(Seg (width (K,a,a,M1,l,n,A))):] is set
[i,n] is set
(K,a,a,M1,l,n,A) * (j,i) is M2( the carrier of a)
M1 * (n,i) is M2( the carrier of a)
A * (M1 * (n,i)) is M2( the carrier of a)
the multF of a . (A,(M1 * (n,i))) is M2( the carrier of a)
M1 * (l,i) is M2( the carrier of a)
(A * (M1 * (n,i))) + (M1 * (l,i)) is M2( the carrier of a)
the addF of a . ((A * (M1 * (n,i))),(M1 * (l,i))) is M2( the carrier of a)
(A * (M * (i,n))) + (M1 * (l,i)) is M2( the carrier of a)
the addF of a . ((A * (M * (i,n))),(M1 * (l,i))) is M2( the carrier of a)
(K,a,a,M1,l,n,A) * (j,i) is M2( the carrier of a)
M1 * (j,i) is M2( the carrier of a)
Indices (K,a,a,M,l,n,A) is set
dom (K,a,a,M,l,n,A) is M2( bool NAT)
width (K,a,a,M,l,n,A) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (K,a,a,M,l,n,A)) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (K,a,a,M,l,n,A) ) } is set
[:(dom (K,a,a,M,l,n,A)),(Seg (width (K,a,a,M,l,n,A))):] is set
Indices M is set
[:(dom M),(Seg (width M)):] is set
i is V21() V22() V23() V27() ext-real non negative set
j is V21() V22() V23() V27() ext-real non negative set
[i,j] is set
(K,a,a,M,l,n,A) * (i,j) is M2( the carrier of a)
((K,a,a,M1,l,n,A) @) * (i,j) is M2( the carrier of a)
M * (i,n) is M2( the carrier of a)
A * (M * (i,n)) is M2( the carrier of a)
the multF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) V155( the carrier of a) M2( bool [:[: the carrier of a, the carrier of a:], the carrier of a:])
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the multF of a . (A,(M * (i,n))) is M2( the carrier of a)
M * (i,l) is M2( the carrier of a)
(A * (M * (i,n))) + (M * (i,l)) is M2( the carrier of a)
the addF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) V155( the carrier of a) V156( the carrier of a) M2( bool [:[: the carrier of a, the carrier of a:], the carrier of a:])
the addF of a . ((A * (M * (i,n))),(M * (i,l))) is M2( the carrier of a)
M * (i,j) is M2( the carrier of a)
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of a is V11() non trivial set
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
1. (a,n) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
dom (1. (a,n)) is M2( bool NAT)
(n,n,a,(1. (a,n)),l,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
a is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
a * (n,n,a,(1. (a,n)),l,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,a,l,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
len (1. (a,n)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (1. (a,n)) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (1. (a,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (1. (a,n)) ) } is set
a @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
width (a @) is V21() V22() V23() V27() ext-real non negative M2( NAT )
(n,n,a,(1. (a,n)),l,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
width (n,n,a,(1. (a,n)),l,K) is V21() V22() V23() V27() ext-real non negative M2( NAT )
len (a @) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len a is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width a is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width a) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width a ) } is set
(n,n,a,(a @),l,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(a @),l,K) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K) * (a @) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
((n,n,a,(1. (a,n)),l,K) * (a @)) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(a @) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
((a @) @) * ((n,n,a,(1. (a,n)),l,K) @) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
a * ((n,n,a,(1. (a,n)),l,K) @) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(1. (a,n)) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,((1. (a,n)) @),l,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,((1. (a,n)) @),l,K) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
a * ((n,n,a,((1. (a,n)) @),l,K) @) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
1. (K,n) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
dom (1. (K,n)) is M2( bool NAT)
a is M2( the carrier of K)
(n,n,K,(1. (K,n)),l,a) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
a is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
a * (n,n,K,(1. (K,n)),l,a) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,a,l,a) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
len (1. (K,n)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (1. (K,n)) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (1. (K,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (1. (K,n)) ) } is set
a @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
width (a @) is V21() V22() V23() V27() ext-real non negative M2( NAT )
(n,n,K,(1. (K,n)),l,a) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
width (n,n,K,(1. (K,n)),l,a) is V21() V22() V23() V27() ext-real non negative M2( NAT )
len (a @) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len a is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width a is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width a) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width a ) } is set
(n,n,K,(a @),l,a) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,(a @),l,a) @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,(1. (K,n)),l,a) * (a @) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
((n,n,K,(1. (K,n)),l,a) * (a @)) @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(a @) @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,(1. (K,n)),l,a) @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
((a @) @) * ((n,n,K,(1. (K,n)),l,a) @) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
a * ((n,n,K,(1. (K,n)),l,a) @) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(1. (K,n)) @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,((1. (K,n)) @),l,a) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,((1. (K,n)) @),l,a) @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
a * ((n,n,K,((1. (K,n)) @),l,a) @) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of a is V11() non trivial set
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
1. (a,n) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
dom (1. (a,n)) is M2( bool NAT)
a is M2( the carrier of a)
(n,n,a,(1. (a,n)),l,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
A is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
A * (n,n,a,(1. (a,n)),l,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,A,l,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
len (1. (a,n)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (1. (a,n)) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (1. (a,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (1. (a,n)) ) } is set
A @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
width (A @) is V21() V22() V23() V27() ext-real non negative M2( NAT )
(n,n,a,(1. (a,n)),l,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
width (n,n,a,(1. (a,n)),l,K,a) is V21() V22() V23() V27() ext-real non negative M2( NAT )
len (A @) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
len A is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width A is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width A) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width A ) } is set
(n,n,a,(A @),l,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(A @),l,K,a) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K,a) * (A @) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
((n,n,a,(1. (a,n)),l,K,a) * (A @)) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(A @) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K,a) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
((A @) @) * ((n,n,a,(1. (a,n)),l,K,a) @) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
A * ((n,n,a,(1. (a,n)),l,K,a) @) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(1. (a,n)) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,((1. (a,n)) @),l,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,((1. (a,n)) @),l,K,a) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
A * ((n,n,a,((1. (a,n)) @),l,K,a) @) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
1. (a,n) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
the carrier of a is V11() non trivial set
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
dom (1. (a,n)) is M2( bool NAT)
(n,n,a,(1. (a,n)),l,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K) ~ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K) ~ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
len (1. (a,n)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (1. (a,n)) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (1. (a,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (1. (a,n)) ) } is set
(1. (a,n)) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
((n,n,a,(1. (a,n)),l,K) @) ~ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,((1. (a,n)) @),l,K) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,((1. (a,n)) @),l,K) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
((n,n,a,((1. (a,n)) @),l,K) @) ~ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V21() V22() V23() V27() ext-real non negative set
a is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of a is V11() non trivial set
1. (a,n) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
the carrier of a * is functional FinSequence-membered FinSequenceSet of the carrier of a
dom (1. (a,n)) is M2( bool NAT)
a is M2( the carrier of a)
(n,n,a,(1. (a,n)),l,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K,a) ~ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
- a is M2( the carrier of a)
(n,n,a,(1. (a,n)),l,K,(- a)) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K,a) ~ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K,(- a)) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
len (1. (a,n)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (1. (a,n)) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (1. (a,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (1. (a,n)) ) } is set
(1. (a,n)) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K,(- a)) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,(1. (a,n)),l,K,a) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
((n,n,a,(1. (a,n)),l,K,a) @) ~ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,((1. (a,n)) @),l,K,a) is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
(n,n,a,((1. (a,n)) @),l,K,a) @ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
((n,n,a,((1. (a,n)) @),l,K,a) @) ~ is V1() V4( NAT ) V5( the carrier of a * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of a
l is V21() V22() V23() V27() ext-real non negative set
n is V21() V22() V23() V27() ext-real non negative set
K is V40() non degenerated non trivial right_complementable almost_left_invertible unital V113() V115() V118() V119() V120() right-distributive left-distributive right_unital well-unital V132() left_unital V182() doubleLoopStr
the carrier of K is V11() non trivial set
1. (K,n) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
dom (1. (K,n)) is M2( bool NAT)
0. K is V47(K) M2( the carrier of K)
a is M2( the carrier of K)
(n,n,K,(1. (K,n)),l,a) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,(1. (K,n)),l,a) ~ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
a " is M2( the carrier of K)
(n,n,K,(1. (K,n)),l,(a ")) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,(1. (K,n)),l,a) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,(1. (K,n)),l,a) ~ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,(1. (K,n)),l,(a ")) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
len (1. (K,n)) is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )
width (1. (K,n)) is V21() V22() V23() V27() ext-real non negative M2( NAT )
Seg (width (1. (K,n))) is M2( bool NAT)
{ b₁ where b₁ is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b₁ & b₁ <= width (1. (K,n)) ) } is set
(1. (K,n)) @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,(1. (K,n)),l,(a ")) @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,(1. (K,n)),l,a) @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
((n,n,K,(1. (K,n)),l,a) @) ~ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,((1. (K,n)) @),l,a) is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
(n,n,K,((1. (K,n)) @),l,a) @ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K
((n,n,K,((1. (K,n)) @),l,a) @) ~ is V1() V4( NAT ) V5( the carrier of K * ) Function-like FinSequence-like tabular Matrix of n,n, the carrier of K