:: MATRIX_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for n, k being Nat st n = n + k holds
k = 0
by XCMPLX_1:3;

definition
let K be Field;
let n, m be Nat;
func 0. K,n,m -> Matrix of n,m,K equals :: MATRIX_3:def 1
n |-> (m |-> (0. K));
coherence
n |-> (m |-> (0. K)) is Matrix of n,m,K
by MATRIX_1:10;
end;

:: deftheorem defines 0. MATRIX_3:def 1 :
for K being Field
for n, m being Nat holds 0. K,n,m = n |-> (m |-> (0. K));

definition
let K be Field;
let A be Matrix of K;
func - A -> Matrix of K means :Def2: :: MATRIX_3:def 2
( len it = len A & width it = width A & ( for i, j being Nat st [i,j] in Indices A holds
it * i,j = - (A * i,j) ) );
existence
ex b1 being Matrix of K st
( len b1 = len A & width b1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b1 * i,j = - (A * i,j) ) )
proof end;
uniqueness
for b1, b2 being Matrix of K st len b1 = len A & width b1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b1 * i,j = - (A * i,j) ) & len b2 = len A & width b2 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b2 * i,j = - (A * i,j) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines - MATRIX_3:def 2 :
for K being Field
for A, b3 being Matrix of K holds
( b3 = - A iff ( len b3 = len A & width b3 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b3 * i,j = - (A * i,j) ) ) );

definition
let K be Field;
let A, B be Matrix of K;
func A + B -> Matrix of K means :Def3: :: MATRIX_3:def 3
( len it = len A & width it = width A & ( for i, j being Nat st [i,j] in Indices A holds
it * i,j = (A * i,j) + (B * i,j) ) );
existence
ex b1 being Matrix of K st
( len b1 = len A & width b1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b1 * i,j = (A * i,j) + (B * i,j) ) )
proof end;
uniqueness
for b1, b2 being Matrix of K st len b1 = len A & width b1 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b1 * i,j = (A * i,j) + (B * i,j) ) & len b2 = len A & width b2 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b2 * i,j = (A * i,j) + (B * i,j) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines + MATRIX_3:def 3 :
for K being Field
for A, B, b4 being Matrix of K holds
( b4 = A + B iff ( len b4 = len A & width b4 = width A & ( for i, j being Nat st [i,j] in Indices A holds
b4 * i,j = (A * i,j) + (B * i,j) ) ) );

theorem :: MATRIX_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MATRIX_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: MATRIX_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for K being Field
for i, j being Nat st [i,j] in Indices (0. K,n,m) holds
(0. K,n,m) * i,j = 0. K
proof end;

theorem :: MATRIX_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for A, B being Matrix of K st len A = len B & width A = width B holds
A + B = B + A
proof end;

theorem :: MATRIX_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for A, B, C being Matrix of K st len A = len B & len A = len C & width A = width B & width A = width C holds
(A + B) + C = A + (B + C)
proof end;

theorem :: MATRIX_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for K being Field
for A being Matrix of n,m,K holds A + (0. K,n,m) = A
proof end;

theorem :: MATRIX_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for K being Field
for A being Matrix of n,m,K holds A + (- A) = 0. K,n,m
proof end;

definition
let K be Field;
let A, B be Matrix of K;
assume A1: width A = len B ;
func A * B -> Matrix of K means :Def4: :: MATRIX_3:def 4
( len it = len A & width it = width B & ( for i, j being Nat st [i,j] in Indices it holds
it * i,j = (Line A,i) "*" (Col B,j) ) );
existence
ex b1 being Matrix of K st
( len b1 = len A & width b1 = width B & ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * i,j = (Line A,i) "*" (Col B,j) ) )
proof end;
uniqueness
for b1, b2 being Matrix of K st len b1 = len A & width b1 = width B & ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * i,j = (Line A,i) "*" (Col B,j) ) & len b2 = len A & width b2 = width B & ( for i, j being Nat st [i,j] in Indices b2 holds
b2 * i,j = (Line A,i) "*" (Col B,j) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines * MATRIX_3:def 4 :
for K being Field
for A, B being Matrix of K st width A = len B holds
for b4 being Matrix of K holds
( b4 = A * B iff ( len b4 = len A & width b4 = width B & ( for i, j being Nat st [i,j] in Indices b4 holds
b4 * i,j = (Line A,i) "*" (Col B,j) ) ) );

definition
let n, k, m be Nat;
let K be Field;
let A be Matrix of n,k,K;
let B be Matrix of width A,m,K;
:: original: *
redefine func A * B -> Matrix of len A, width B,K;
coherence
A * B is Matrix of len A, width B,K
proof end;
end;

definition
let K be Field;
let M be Matrix of K;
let a be Element of K;
func a * M -> Matrix of K means :: MATRIX_3:def 5
( len it = len M & width it = width M & ( for i, j being Nat st [i,j] in Indices M holds
it * i,j = a * (M * i,j) ) );
existence
ex b1 being Matrix of K st
( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * i,j = a * (M * i,j) ) )
proof end;
uniqueness
for b1, b2 being Matrix of K st len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * i,j = a * (M * i,j) ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b2 * i,j = a * (M * i,j) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines * MATRIX_3:def 5 :
for K being Field
for M being Matrix of K
for a being Element of K
for b4 being Matrix of K holds
( b4 = a * M iff ( len b4 = len M & width b4 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b4 * i,j = a * (M * i,j) ) ) );

definition
let K be Field;
let M be Matrix of K;
let a be Element of K;
func M * a -> Matrix of K equals :: MATRIX_3:def 6
a * M;
coherence
a * M is Matrix of K
;
end;

:: deftheorem defines * MATRIX_3:def 6 :
for K being Field
for M being Matrix of K
for a being Element of K holds M * a = a * M;

theorem :: MATRIX_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for p, q being FinSequence of K st len p = len q holds
( len (mlt p,q) = len p & len (mlt p,q) = len q )
proof end;

theorem :: MATRIX_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for K being Field
for i, l being Nat st [i,l] in Indices (1. K,n) & l = i holds
(Line (1. K,n),i) . l = 1. K
proof end;

theorem :: MATRIX_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for K being Field
for i, l being Nat st [i,l] in Indices (1. K,n) & l <> i holds
(Line (1. K,n),i) . l = 0. K
proof end;

theorem :: MATRIX_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for K being Field
for l, j being Nat st [l,j] in Indices (1. K,n) & l = j holds
(Col (1. K,n),j) . l = 1. K
proof end;

theorem :: MATRIX_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for K being Field
for l, j being Nat st [l,j] in Indices (1. K,n) & l <> j holds
(Col (1. K,n),j) . l = 0. K
proof end;

Lm2: for L being non empty add-associative right_zeroed right_complementable LoopStr
for p being FinSequence of L st ( for i being Nat st i in dom p holds
p . i = 0. L ) holds
Sum p = 0. L
proof end;

theorem Th13: :: MATRIX_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for K being non empty add-associative right_zeroed right_complementable LoopStr holds Sum (n |-> (0. K)) = 0. K
proof end;

theorem Th14: :: MATRIX_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable LoopStr
for p being FinSequence of K
for i being Nat st i in dom p & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
Sum p = p . i
proof end;

theorem Th15: :: MATRIX_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for p, q being FinSequence of K holds len (mlt p,q) = min (len p),(len q)
proof end;

theorem Th16: :: MATRIX_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for p, q being FinSequence of K
for i being Nat st i in dom p & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
for j being Nat st j in dom (mlt p,q) holds
( ( i = j implies (mlt p,q) . j = q . i ) & ( i <> j implies (mlt p,q) . j = 0. K ) )
proof end;

theorem Th17: :: MATRIX_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for K being Field
for i, j being Nat st [i,j] in Indices (1. K,n) holds
( ( i = j implies (Line (1. K,n),i) . j = 1. K ) & ( i <> j implies (Line (1. K,n),i) . j = 0. K ) )
proof end;

theorem Th18: :: MATRIX_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for K being Field
for i, j being Nat st [i,j] in Indices (1. K,n) holds
( ( i = j implies (Col (1. K,n),j) . i = 1. K ) & ( i <> j implies (Col (1. K,n),j) . i = 0. K ) )
proof end;

theorem Th19: :: MATRIX_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for p, q being FinSequence of K
for i being Nat st i in dom p & i in dom q & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
Sum (mlt p,q) = q . i
proof end;

theorem :: MATRIX_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for K being Field
for A being Matrix of n,K holds (1. K,n) * A = A
proof end;

theorem :: MATRIX_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for K being Field
for A being Matrix of n,K holds A * (1. K,n) = A
proof end;

theorem :: MATRIX_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for a, b being Element of K holds <*<*a*>*> * <*<*b*>*> = <*<*(a * b)*>*>
proof end;

theorem :: MATRIX_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for a1, a2, b1, b2, c1, c2, d1, d2 being Element of K holds (a1,b1 ][ c1,d1) * (a2,b2 ][ c2,d2) = ((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2)) ][ ((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2))
proof end;

theorem :: MATRIX_3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for A, B being Matrix of K st width A = len B & width B <> 0 holds
(A * B) @ = (B @ ) * (A @ )
proof end;

definition
let I, J be non empty set ;
let X be Element of Fin I;
let Y be Element of Fin J;
:: original: [:
redefine func [:X,Y:] -> Element of Fin [:I,J:];
coherence
[:X,Y:] is Element of Fin [:I,J:]
proof end;
end;

definition
let I, J, D be non empty set ;
let G be BinOp of D;
let f be Function of I,D;
let g be Function of J,D;
:: original: *
redefine func G * f,g -> Function of [:I,J:],D;
coherence
G * f,g is Function of [:I,J:],D
by FINSEQOP:84;
end;

theorem Th25: :: MATRIX_3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J, D being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F has_a_unity ) & G is commutative holds
F $$ [:X,Y:],(G * f,g) = F $$ [:Y,X:],(G * g,f)
proof end;

theorem Th26: :: MATRIX_3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D st F is commutative & F is associative & F has_a_unity holds
for x being Element of I
for y being Element of J holds F $$ [:{x},{y}:],(G * f,g) = F $$ {x},(G [:] f,(F $$ {y},g))
proof end;

theorem Th27: :: MATRIX_3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & F has_a_unity & F has_an_inverseOp & G is_distributive_wrt F holds
for x being Element of I holds F $$ [:{x},Y:],(G * f,g) = F $$ {x},(G [:] f,(F $$ Y,g))
proof end;

theorem Th28: :: MATRIX_3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F has_a_unity & F is commutative & F is associative & F has_an_inverseOp & G is_distributive_wrt F holds
F $$ [:X,Y:],(G * f,g) = F $$ X,(G [:] f,(F $$ Y,g))
proof end;

theorem :: MATRIX_3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D st F is commutative & F is associative & F has_a_unity & G is commutative holds
for x being Element of I
for y being Element of J holds F $$ [:{x},{y}:],(G * f,g) = F $$ {y},(G [;] (F $$ {x},f),g)
proof end;

theorem :: MATRIX_3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F has_a_unity & F is commutative & F is associative & F has_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ [:X,Y:],(G * f,g) = F $$ Y,(G [;] (F $$ X,f),g)
proof end;

theorem Th31: :: MATRIX_3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for Y being Element of Fin J st F has_a_unity & F is commutative & F is associative & F has_an_inverseOp holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) holds
F $$ [:{x},Y:],f = F $$ {x},g
proof end;

theorem Th32: :: MATRIX_3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for X being Element of Fin I
for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) & F has_a_unity & F is commutative & F is associative & F has_an_inverseOp holds
F $$ [:X,Y:],f = F $$ X,g
proof end;

theorem Th33: :: MATRIX_3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I st F has_a_unity & F is commutative & F is associative & F has_an_inverseOp holds
for y being Element of J st ( for j being Element of J holds g . j = F $$ X,((curry' f) . j) ) holds
F $$ [:X,{y}:],f = F $$ {y},g
proof end;

theorem Th34: :: MATRIX_3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ X,((curry' f) . j) ) & F has_a_unity & F is commutative & F is associative & F has_an_inverseOp holds
F $$ [:X,Y:],f = F $$ Y,g
proof end;

theorem :: MATRIX_3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for A, B, C being Matrix of K st width A = len B & width B = len C holds
(A * B) * C = A * (B * C)
proof end;

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
let p be Element of Permutations n;
func Path_matrix p,M -> FinSequence of K means :Def7: :: MATRIX_3:def 7
( len it = n & ( for i, j being Nat st i in dom it & j = p . i holds
it . i = M * i,j ) );
existence
ex b1 being FinSequence of K st
( len b1 = n & ( for i, j being Nat st i in dom b1 & j = p . i holds
b1 . i = M * i,j ) )
proof end;
uniqueness
for b1, b2 being FinSequence of K st len b1 = n & ( for i, j being Nat st i in dom b1 & j = p . i holds
b1 . i = M * i,j ) & len b2 = n & ( for i, j being Nat st i in dom b2 & j = p . i holds
b2 . i = M * i,j ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Path_matrix MATRIX_3:def 7 :
for n being Nat
for K being Field
for M being Matrix of n,K
for p being Element of Permutations n
for b5 being FinSequence of K holds
( b5 = Path_matrix p,M iff ( len b5 = n & ( for i, j being Nat st i in dom b5 & j = p . i holds
b5 . i = M * i,j ) ) );

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
func Path_product M -> Function of Permutations n,the carrier of K means :Def8: :: MATRIX_3:def 8
for p being Element of Permutations n holds it . p = - (the mult of K $$ (Path_matrix p,M)),p;
existence
ex b1 being Function of Permutations n,the carrier of K st
for p being Element of Permutations n holds b1 . p = - (the mult of K $$ (Path_matrix p,M)),p
proof end;
uniqueness
for b1, b2 being Function of Permutations n,the carrier of K st ( for p being Element of Permutations n holds b1 . p = - (the mult of K $$ (Path_matrix p,M)),p ) & ( for p being Element of Permutations n holds b2 . p = - (the mult of K $$ (Path_matrix p,M)),p ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Path_product MATRIX_3:def 8 :
for n being Nat
for K being Field
for M being Matrix of n,K
for b4 being Function of Permutations n,the carrier of K holds
( b4 = Path_product M iff for p being Element of Permutations n holds b4 . p = - (the mult of K $$ (Path_matrix p,M)),p );

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
func Det M -> Element of K equals :: MATRIX_3:def 9
the add of K $$ (FinOmega (Permutations n)),(Path_product M);
coherence
the add of K $$ (FinOmega (Permutations n)),(Path_product M) is Element of K
;
end;

:: deftheorem defines Det MATRIX_3:def 9 :
for n being Nat
for K being Field
for M being Matrix of n,K holds Det M = the add of K $$ (FinOmega (Permutations n)),(Path_product M);

theorem :: MATRIX_3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for a being Element of K holds Det <*<*a*>*> = a
proof end;

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
func diagonal_of_Matrix M -> FinSequence of K means :: MATRIX_3:def 10
( len it = n & ( for i being Nat st i in Seg n holds
it . i = M * i,i ) );
existence
ex b1 being FinSequence of K st
( len b1 = n & ( for i being Nat st i in Seg n holds
b1 . i = M * i,i ) )
proof end;
uniqueness
for b1, b2 being FinSequence of K st len b1 = n & ( for i being Nat st i in Seg n holds
b1 . i = M * i,i ) & len b2 = n & ( for i being Nat st i in Seg n holds
b2 . i = M * i,i ) holds
b1 = b2
proof end;
end;

:: deftheorem defines diagonal_of_Matrix MATRIX_3:def 10 :
for n being Nat
for K being Field
for M being Matrix of n,K
for b4 being FinSequence of K holds
( b4 = diagonal_of_Matrix M iff ( len b4 = n & ( for i being Nat st i in Seg n holds
b4 . i = M * i,i ) ) );