:: MATRIX12 semantic presentation

REAL is set
NAT is V11() V21() V22() V23() M2( bool REAL)

NAT is V11() V21() V22() V23() 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= n ) } is set

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 () is M2( bool NAT)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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 () -tuples_on the carrier of K
() -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 () -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 () -tuples_on the carrier of K
() -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 () -tuples_on the carrier of K
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
() -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 () -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

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 () is M2( bool NAT)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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 () -tuples_on the carrier of K
() -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 () -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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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 () is M2( bool NAT)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg ()):] is set
Indices a is set
[:(dom a),(Seg ()):] 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

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

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 () -tuples_on the carrier of a
width A is V21() V22() V23() V27() ext-real non negative M2( NAT )
() -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 () -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 () -tuples_on the carrier of a
width M is V21() V22() V23() V27() ext-real non negative M2( NAT )
() -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 () -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 () is M2( bool NAT)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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 () is M2( bool NAT)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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 () is M2( bool NAT)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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

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 () is M2( bool NAT)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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 () -tuples_on the carrier of K
() -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 () -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)),()) 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 ()):] 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= n ) } is set

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 () is M2( bool NAT)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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 () -tuples_on the carrier of K
() -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,()) 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 () -tuples_on the carrier of K
K174( the carrier of K, the carrier of K,(Line (A,a)),()) 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 () -tuples_on the carrier of K
() -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 () -tuples_on the carrier of K
K174( the carrier of K, the carrier of K,(Line (A,a)),()) 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 () -tuples_on the carrier of K
() -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 () -tuples_on the carrier of K
(Line (A,M2)) . i is set

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 () is M2( bool NAT)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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 () -tuples_on the carrier of K
() -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 () -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)),()) 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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 () is M2( bool NAT)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg ()):] is set
Indices a is set
[:(dom a),(Seg ()):] 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

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 () -tuples_on the carrier of a
() -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 () -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)),()) 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 () -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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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

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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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,()) 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)),()) 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 () -tuples_on the carrier of M
() -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 () -tuples_on the carrier of M
() -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

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 () is M2( bool NAT)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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 () -tuples_on the carrier of K
() -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 () -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 () -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)),()) 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 () -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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= width M1 ) } is set
[:(dom M1),(Seg (width M1)):] is set
Indices a is set
[:(dom a),(Seg ()):] 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

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)),()) 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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 )

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

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

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

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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= len (1. (a,n)) ) } is set
Seg (len a) is M2( bool NAT)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= len (1. (a,n)) ) } is set
Seg (len a) is M2( bool NAT)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= len (1. (a,n)) ) } is set
Seg (len a) is M2( bool NAT)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT ) : ( 1 <= b1 & b1 <= 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

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()