:: 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

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

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

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

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

[:(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

(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

(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

(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

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

len M is V21() V22() V23() V27() ext-real non negative M3( REAL , NAT )

Seg (len M) is M2( bool NAT)

{ b

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

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

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

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

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

[:(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

(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

(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

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

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

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

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

[:(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

(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

(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

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

[:(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

[:(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

[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

Seg (len a) is M2( bool NAT)

{ b

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

[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

[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

Seg (len a) is M2( bool NAT)

{ b

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

[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

Seg (len a) is M2( bool NAT)

{ b

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

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