:: Matrices. Abelian Group of Matrices
:: by Katarzyna Jankowska
::
:: Received June 8, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

definition
let f be FinSequence;
attrf is tabular  means :Def1: :: MATRIX_1:def 1
 ex n being Nat st
for x being set st x in rng f holds
ex s being FinSequence st
( s = x & len s = n );
end;

:: deftheorem Def1 defines tabular MATRIX_1:def_1_:_
 for f being FinSequence holds
( f is tabular iff ex n being Nat st
for x being set st x in rng f holds
ex s being FinSequence st
( s = x & len s = n ) );

registration
cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V172() tabular for set ;
existence
 ex b1 being FinSequence st b1 is tabular
proofend;
end;

theorem Th1: :: MATRIX_1:1
for D being non empty set
for d being Element of D holds <*<*d*>*> is tabular
proofend;

theorem Th2: :: MATRIX_1:2
for x being set
for m, n being Nat holds m |-> (n |-> x) is tabular
proofend;

theorem Th3: :: MATRIX_1:3
for s being FinSequence holds <*s*> is tabular
proofend;

theorem Th4: :: MATRIX_1:4
for n being Nat
for s1, s2 being FinSequence st len s1 = n &amp; len s2 = n holds
<*s1,s2*> is tabular
proofend;

theorem Th5: :: MATRIX_1:5
{} is tabular
proofend;

theorem :: MATRIX_1:6
<*{},{}*> is tabular by Th4, CARD_1:27;

theorem :: MATRIX_1:7
for D being non empty set
for a1, a2 being Element of D holds <*<*a1*>,<*a2*>*> is tabular
proofend;

theorem :: MATRIX_1:8
for D being non empty set
for a1, a2, b1, b2 being Element of D holds <*<*a1,a2*>,<*b1,b2*>*> is tabular
proofend;

registration
let D be set ;
cluster Relation-like NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() tabular for FinSequence of D * ;
existence
 ex b1 being FinSequence of D * st b1 is tabular
proofend;
end;

definition
let D be set ;
mode Matrix of D is tabular FinSequence of D * ;
end;

registration
let D be non empty set ;
cluster Relation-like non empty-yielding NAT -defined D * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() tabular for FinSequence of D * ;
existence
 not for b1 being Matrix of D holds b1 is empty-yielding
proofend;
end;

theorem Th9: :: MATRIX_1:9
for D being non empty set
for s being FinSequence holds
( s is Matrix of D iff ex n being Nat st
for x being set st x in rng s holds
ex p being FinSequence of D st
( x = p &amp; len p = n ) )
proofend;

definition
let D be non empty set ;
let m, n be Nat;
mode Matrix of m,n,D ->  Matrix of D means :Def2: :: MATRIX_1:def 2
( len it = m &amp; ( for p being FinSequence of D st p in rng it holds
len p = n ) );
existence
 ex b1 being Matrix of D st
( len b1 = m &amp; ( for p being FinSequence of D st p in rng b1 holds
len p = n ) )
proofend;
end;

:: deftheorem Def2 defines Matrix MATRIX_1:def_2_:_
 for D being non empty set
for m, n being Nat
for b4 being Matrix of D holds
( b4 is Matrix of m,n,D iff ( len b4 = m &amp; ( for p being FinSequence of D st p in rng b4 holds
len p = n ) ) );

definition
let D be non empty set ;
let n be Nat;
mode Matrix of n,D is Matrix of n,n,D;
end;

definition
let K be non empty 1-sorted ;
mode Matrix of K is Matrix of the carrier of K;
let n be Nat;
mode Matrix of n,K is Matrix of n,n, the carrier of K;
let m be Nat;
mode Matrix of n,m,K is Matrix of n,m, the carrier of K;
end;

theorem Th10: :: MATRIX_1:10
for m, n being Nat
for D being non empty set
for a being Element of D holds m |-> (n |-> a) is Matrix of m,n,D
proofend;

theorem Th11: :: MATRIX_1:11
for D being non empty set
for p being FinSequence of D holds <*p*> is Matrix of 1, len p,D
proofend;

theorem Th12: :: MATRIX_1:12
for n being Nat
for D being non empty set
for p1, p2 being FinSequence of D st len p1 = n &amp; len p2 = n holds
<*p1,p2*> is Matrix of 2,n,D
proofend;

theorem Th13: :: MATRIX_1:13
for m being Nat
for D being non empty set holds {} is Matrix of 0 ,m,D
proofend;

theorem :: MATRIX_1:14
for D being non empty set holds <*{}*> is Matrix of 1, 0 ,D
proofend;

theorem :: MATRIX_1:15
for D being non empty set
for a being Element of D holds <*<*a*>*> is Matrix of 1,D
proofend;

theorem :: MATRIX_1:16
for D being non empty set holds <*{},{}*> is Matrix of 2, 0 ,D
proofend;

theorem :: MATRIX_1:17
for D being non empty set
for a1, a2 being Element of D holds <*<*a1,a2*>*> is Matrix of 1,2,D
proofend;

theorem :: MATRIX_1:18
for D being non empty set
for a1, a2 being Element of D holds <*<*a1*>,<*a2*>*> is Matrix of 2,1,D
proofend;

theorem :: MATRIX_1:19
for D being non empty set
for a1, a2, b1, b2 being Element of D holds <*<*a1,a2*>,<*b1,b2*>*> is Matrix of 2,D
proofend;

definition
let M be tabular FinSequence;
func width M ->  Element of NAT  means :Def3: :: MATRIX_1:def 3
 ex s being FinSequence st
( s in rng M &amp; len s = it ) if  len M > 0
otherwise it = 0 ;
existence
 ( ( len M > 0 implies ex b1 being Element of NAT ex s being FinSequence st
( s in rng M &amp; len s = b1 ) ) &amp; ( not len M > 0 implies ex b1 being Element of NAT st b1 = 0 ) )
proofend;
uniqueness
 for b1, b2 being Element of NAT holds
( ( len M > 0 &amp; ex s being FinSequence st
( s in rng M &amp; len s = b1 ) &amp; ex s being FinSequence st
( s in rng M &amp; len s = b2 ) implies b1 = b2 ) &amp; ( not len M > 0 &amp; b1 = 0 &amp; b2 = 0 implies b1 = b2 ) )
proofend;
consistency
 for b1 being Element of NAT holds verum ;
end;

:: deftheorem Def3 defines width MATRIX_1:def_3_:_
 for M being tabular FinSequence
for b2 being Element of NAT holds
( ( len M > 0 implies ( b2 = width M iff ex s being FinSequence st
( s in rng M &amp; len s = b2 ) ) ) &amp; ( not len M > 0 implies ( b2 = width M iff b2 = 0 ) ) );

theorem Th20: :: MATRIX_1:20
for D being non empty set
for M being Matrix of D st len M > 0 holds
for n being Nat holds
( M is Matrix of len M,n,D iff n = width M )
proofend;

definition
let M be tabular FinSequence;
func Indices M ->  set  equals :: MATRIX_1:def 4
[:(dom M),(Seg (width M)):];
coherence
 [:(dom M),(Seg (width M)):] is set ;
end;

:: deftheorem  defines Indices MATRIX_1:def_4_:_
 for M being tabular FinSequence holds Indices M = [:(dom M),(Seg (width M)):];

definition
let D be set ;
let M be Matrix of D;
let i, j be Nat;
assume A1: [i,j] in Indices M ;
funcM * (i,j) ->  Element of D means :Def5: :: MATRIX_1:def 5
 ex p being FinSequence of D st
( p = M . i &amp; it = p . j );
existence
 ex b1 being Element of D ex p being FinSequence of D st
( p = M . i &amp; b1 = p . j )
proofend;
uniqueness
 for b1, b2 being Element of D st ex p being FinSequence of D st
( p = M . i &amp; b1 = p . j ) &amp; ex p being FinSequence of D st
( p = M . i &amp; b2 = p . j ) holds
b1 = b2 ;
end;

:: deftheorem Def5 defines * MATRIX_1:def_5_:_
 for D being set
for M being Matrix of D
for i, j being Nat st [i,j] in Indices M holds
for b5 being Element of D holds
( b5 = M * (i,j) iff ex p being FinSequence of D st
( p = M . i &amp; b5 = p . j ) );

theorem Th21: :: MATRIX_1:21
for D being non empty set
for M1, M2 being Matrix of D st len M1 = len M2 &amp; width M1 = width M2 &amp; ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) ) holds
M1 = M2
proofend;

scheme :: MATRIX_1:sch 1
MatrixLambda{ F1() ->  non empty set , F2() ->  Element of NAT , F3() ->  Element of NAT , F4( set , set ) ->  Element of F1() } :
 ex M being Matrix of F2(),F3(),F1() st
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = F4(i,j)
proofend;

scheme :: MATRIX_1:sch 2
MatrixEx{ F1() ->  non empty set , F2() ->  Element of NAT , F3() ->  Element of NAT , P1[ set , set , set ] } :
 ex M being Matrix of F2(),F3(),F1() st
for i, j being Nat st [i,j] in Indices M holds
P1[i,j,M * (i,j)]
provided
A1: for i, j being Nat st [i,j] in [:(Seg F2()),(Seg F3()):] holds
ex x being Element of F1() st P1[i,j,x]
proofend;

theorem :: MATRIX_1:22
for m being Nat
for D being non empty set
for M being Matrix of 0 ,m,D holds
( len M = 0 &amp; width M = 0 &amp; Indices M = {} )
proofend;

theorem Th23: :: MATRIX_1:23
for n, m being Nat
for D being non empty set st n > 0 holds
for M being Matrix of n,m,D holds
( len M = n &amp; width M = m &amp; Indices M = [:(Seg n),(Seg m):] )
proofend;

theorem Th24: :: MATRIX_1:24
for n being Nat
for D being non empty set
for M being Matrix of n,D holds
( len M = n &amp; width M = n &amp; Indices M = [:(Seg n),(Seg n):] )
proofend;

theorem Th25: :: MATRIX_1:25
for n, m being Nat
for D being non empty set
for M being Matrix of n,m,D holds
( len M = n &amp; Indices M = [:(Seg n),(Seg (width M)):] )
proofend;

theorem Th26: :: MATRIX_1:26
for n, m being Nat
for D being non empty set
for M1, M2 being Matrix of n,m,D holds Indices M1 = Indices M2
proofend;

theorem Th27: :: MATRIX_1:27
for n, m being Nat
for D being non empty set
for M1, M2 being Matrix of n,m,D st ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) ) holds
M1 = M2
proofend;

theorem :: MATRIX_1:28
for n being Nat
for D being non empty set
for M1 being Matrix of n,D
for i, j being Nat st [i,j] in Indices M1 holds
[j,i] in Indices M1
proofend;

definition
let D be non empty set ;
let M be Matrix of D;
funcM @  ->  Matrix of D means :Def6: :: MATRIX_1:def 6
( len it = width M &amp; ( for i, j being Nat holds
( [i,j] in Indices it iff [j,i] in Indices M ) ) &amp; ( for i, j being Nat st [j,i] in Indices M holds
it * (i,j) = M * (j,i) ) );
existence
 ex b1 being Matrix of D st
( len b1 = width M &amp; ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) &amp; ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) )
proofend;
uniqueness
 for b1, b2 being Matrix of D st len b1 = width M &amp; ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) &amp; ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) &amp; len b2 = width M &amp; ( for i, j being Nat holds
( [i,j] in Indices b2 iff [j,i] in Indices M ) ) &amp; ( for i, j being Nat st [j,i] in Indices M holds
b2 * (i,j) = M * (j,i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines @ MATRIX_1:def_6_:_
 for D being non empty set
for M, b3 being Matrix of D holds
( b3 = M @ iff ( len b3 = width M &amp; ( for i, j being Nat holds
( [i,j] in Indices b3 iff [j,i] in Indices M ) ) &amp; ( for i, j being Nat st [j,i] in Indices M holds
b3 * (i,j) = M * (j,i) ) ) );

Lm1:  for D being non empty set
for M being Matrix of D st width M > 0 holds
( len (M @) = width M &amp; width (M @) = len M )
proofend;

Lm2:  for n being Element of NAT
for K being non empty set
for A being Matrix of n,K holds A @ is Matrix of n,K
proofend;

definition
let n be Nat;
let D be non empty set ;
let M be Matrix of n,D;
:: original:@
redefine funcM @  ->  Matrix of n,D;
coherence
 M @ is Matrix of n,D
proofend;
end;

definition
let D be non empty set ;
let M be Matrix of D;
let i be Nat;
func Line (M,i) ->  FinSequence of D means :Def7: :: MATRIX_1:def 7
( len it = width M &amp; ( for j being Nat st j in Seg (width M) holds
it . j = M * (i,j) ) );
existence
 ex b1 being FinSequence of D st
( len b1 = width M &amp; ( for j being Nat st j in Seg (width M) holds
b1 . j = M * (i,j) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of D st len b1 = width M &amp; ( for j being Nat st j in Seg (width M) holds
b1 . j = M * (i,j) ) &amp; len b2 = width M &amp; ( for j being Nat st j in Seg (width M) holds
b2 . j = M * (i,j) ) holds
b1 = b2
proofend;
func Col (M,i) ->  FinSequence of D means :Def8: :: MATRIX_1:def 8
( len it = len M &amp; ( for j being Nat st j in dom M holds
it . j = M * (j,i) ) );
existence
 ex b1 being FinSequence of D st
( len b1 = len M &amp; ( for j being Nat st j in dom M holds
b1 . j = M * (j,i) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of D st len b1 = len M &amp; ( for j being Nat st j in dom M holds
b1 . j = M * (j,i) ) &amp; len b2 = len M &amp; ( for j being Nat st j in dom M holds
b2 . j = M * (j,i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines Line MATRIX_1:def_7_:_
 for D being non empty set
for M being Matrix of D
for i being Nat
for b4 being FinSequence of D holds
( b4 = Line (M,i) iff ( len b4 = width M &amp; ( for j being Nat st j in Seg (width M) holds
b4 . j = M * (i,j) ) ) );

:: deftheorem Def8 defines Col MATRIX_1:def_8_:_
 for D being non empty set
for M being Matrix of D
for i being Nat
for b4 being FinSequence of D holds
( b4 = Col (M,i) iff ( len b4 = len M &amp; ( for j being Nat st j in dom M holds
b4 . j = M * (j,i) ) ) );

definition
let D be non empty set ;
let M be Matrix of D;
let i be Nat;
:: original:Line
redefine func Line (M,i) ->  Element of (width M) -tuples_on D;
coherence
 Line (M,i) is Element of (width M) -tuples_on D
proofend;
:: original:Col
redefine func Col (M,i) ->  Element of (len M) -tuples_on D;
coherence
 Col (M,i) is Element of (len M) -tuples_on D
proofend;
end;

definition
let K be non empty doubleLoopStr ;
let n be Nat;
funcn -Matrices_over K ->  set  equals :: MATRIX_1:def 9
n -tuples_on (n -tuples_on the carrier of K);
coherence
 n -tuples_on (n -tuples_on the carrier of K) is set ;
func 0. (K,n) ->  Matrix of n,K equals :: MATRIX_1:def 10
n |-> (n |-> (0. K));
coherence
 n |-> (n |-> (0. K)) is Matrix of n,K by Th10;
func 1. (K,n) ->  Matrix of n,K means :Def11: :: MATRIX_1:def 11
( ( for i being Nat st [i,i] in Indices it holds
it * (i,i) = 1. K ) &amp; ( for i, j being Nat st [i,j] in Indices it &amp; i <> j holds
it * (i,j) = 0. K ) );
existence
 ex b1 being Matrix of n,K st
( ( for i being Nat st [i,i] in Indices b1 holds
b1 * (i,i) = 1. K ) &amp; ( for i, j being Nat st [i,j] in Indices b1 &amp; i <> j holds
b1 * (i,j) = 0. K ) )
proofend;
uniqueness
 for b1, b2 being Matrix of n,K st ( for i being Nat st [i,i] in Indices b1 holds
b1 * (i,i) = 1. K ) &amp; ( for i, j being Nat st [i,j] in Indices b1 &amp; i <> j holds
b1 * (i,j) = 0. K ) &amp; ( for i being Nat st [i,i] in Indices b2 holds
b2 * (i,i) = 1. K ) &amp; ( for i, j being Nat st [i,j] in Indices b2 &amp; i <> j holds
b2 * (i,j) = 0. K ) holds
b1 = b2
proofend;
let A be Matrix of n,K;
func - A ->  Matrix of n,K means :Def12: :: MATRIX_1:def 12
 for i, j being Nat st [i,j] in Indices A holds
it * (i,j) = - (A * (i,j));
existence
 ex b1 being Matrix of n,K st
for i, j being Nat st [i,j] in Indices A holds
b1 * (i,j) = - (A * (i,j))
proofend;
uniqueness
 for b1, b2 being Matrix of n,K st ( for i, j being Nat st [i,j] in Indices A holds
b1 * (i,j) = - (A * (i,j)) ) &amp; ( for i, j being Nat st [i,j] in Indices A holds
b2 * (i,j) = - (A * (i,j)) ) holds
b1 = b2
proofend;
let B be Matrix of n,K;
funcA + B ->  Matrix of n,K means :Def13: :: MATRIX_1:def 13
 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 n,K st
for i, j being Nat st [i,j] in Indices A holds
b1 * (i,j) = (A * (i,j)) + (B * (i,j))
proofend;
uniqueness
 for b1, b2 being Matrix of n,K st ( for i, j being Nat st [i,j] in Indices A holds
b1 * (i,j) = (A * (i,j)) + (B * (i,j)) ) &amp; ( for i, j being Nat st [i,j] in Indices A holds
b2 * (i,j) = (A * (i,j)) + (B * (i,j)) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines -Matrices_over MATRIX_1:def_9_:_
 for K being non empty doubleLoopStr
for n being Nat holds n -Matrices_over K = n -tuples_on (n -tuples_on the carrier of K);

:: deftheorem  defines 0. MATRIX_1:def_10_:_
 for K being non empty doubleLoopStr
for n being Nat holds 0. (K,n) = n |-> (n |-> (0. K));

:: deftheorem Def11 defines 1. MATRIX_1:def_11_:_
 for K being non empty doubleLoopStr
for n being Nat
for b3 being Matrix of n,K holds
( b3 = 1. (K,n) iff ( ( for i being Nat st [i,i] in Indices b3 holds
b3 * (i,i) = 1. K ) &amp; ( for i, j being Nat st [i,j] in Indices b3 &amp; i <> j holds
b3 * (i,j) = 0. K ) ) );

:: deftheorem Def12 defines - MATRIX_1:def_12_:_
 for K being non empty doubleLoopStr
for n being Nat
for A, b4 being Matrix of n,K holds
( b4 = - A iff for i, j being Nat st [i,j] in Indices A holds
b4 * (i,j) = - (A * (i,j)) );

:: deftheorem Def13 defines + MATRIX_1:def_13_:_
 for K being non empty doubleLoopStr
for n being Nat
for A, B, b5 being Matrix of n,K holds
( b5 = A + B iff for i, j being Nat st [i,j] in Indices A holds
b5 * (i,j) = (A * (i,j)) + (B * (i,j)) );

registration
let K be non empty doubleLoopStr ;
let n be Nat;
clustern -Matrices_over K ->  non empty ;
coherence
 not n -Matrices_over K is empty ;
end;

theorem Th29: :: MATRIX_1:29
for i, j, n being Nat
for K being non empty doubleLoopStr st [i,j] in Indices (0. (K,n)) holds
(0. (K,n)) * (i,j) = 0. K
proofend;

theorem Th30: :: MATRIX_1:30
for x being set
for n being Nat
for K being non empty doubleLoopStr holds
( x is Element of n -Matrices_over K iff x is Matrix of n,K )
proofend;

definition
let K be non empty ZeroStr ;
let M be Matrix of K;
attrM is diagonal  means :: MATRIX_1:def 14
 for i, j being Nat st [i,j] in Indices M &amp; M * (i,j) <> 0. K holds
i = j;
end;

:: deftheorem  defines diagonal MATRIX_1:def_14_:_
 for K being non empty ZeroStr
for M being Matrix of K holds
( M is diagonal iff for i, j being Nat st [i,j] in Indices M &amp; M * (i,j) <> 0. K holds
i = j );

registration
let n be Nat;
let K be non empty doubleLoopStr ;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like V27() finite FinSequence-like FinSubsequence-like countable V171() V172() tabular diagonal for Matrix of n,n, the carrier of K;
existence
 ex b1 being Matrix of n,K st b1 is diagonal
proofend;
end;

definition
let K be non empty doubleLoopStr ;
let n be Nat;
mode Diagonal of n,K is diagonal Matrix of n,K;
end;

theorem Th31: :: MATRIX_1:31
for n being Nat
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A, B being Matrix of n,F holds A + B = B + A
proofend;

theorem Th32: :: MATRIX_1:32
for n being Nat
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A, B, C being Matrix of n,F holds (A + B) + C = A + (B + C)
proofend;

theorem Th33: :: MATRIX_1:33
for n being Nat
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A being Matrix of n,F holds A + (0. (F,n)) = A
proofend;

theorem Th34: :: MATRIX_1:34
for n being Nat
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A being Matrix of n,F holds A + (- A) = 0. (F,n)
proofend;

definition
let F be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ;
let n be Nat;
funcn -G_Matrix_over F ->  strict AbGroup means :: MATRIX_1:def 15
( the carrier of it = n -Matrices_over F &amp; ( for A, B being Matrix of n,F holds the addF of it . (A,B) = A + B ) &amp; 0. it = 0. (F,n) );
existence
 ex b1 being strict AbGroup st
( the carrier of b1 = n -Matrices_over F &amp; ( for A, B being Matrix of n,F holds the addF of b1 . (A,B) = A + B ) &amp; 0. b1 = 0. (F,n) )
proofend;
uniqueness
 for b1, b2 being strict AbGroup st the carrier of b1 = n -Matrices_over F &amp; ( for A, B being Matrix of n,F holds the addF of b1 . (A,B) = A + B ) &amp; 0. b1 = 0. (F,n) &amp; the carrier of b2 = n -Matrices_over F &amp; ( for A, B being Matrix of n,F holds the addF of b2 . (A,B) = A + B ) &amp; 0. b2 = 0. (F,n) holds
b1 = b2
proofend;
end;

:: deftheorem  defines -G_Matrix_over MATRIX_1:def_15_:_
 for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for n being Nat
for b3 being strict AbGroup holds
( b3 = n -G_Matrix_over F iff ( the carrier of b3 = n -Matrices_over F &amp; ( for A, B being Matrix of n,F holds the addF of b3 . (A,B) = A + B ) &amp; 0. b3 = 0. (F,n) ) );

theorem :: MATRIX_1:35
for n, m being Nat
for K being non empty doubleLoopStr
for M1 being Matrix of 0 ,n,K
for M2 being Matrix of 0 ,m,K holds M1 = M2
proofend;

begin

:: from GOBOARD7, 2008.02.21, A.T.
theorem Th36: :: MATRIX_1:36
for D being set
for i, j being Nat
for M being Matrix of D st 1 <= i &amp; i <= len M &amp; 1 <= j &amp; j <= width M holds
[i,j] in Indices M
proofend;

theorem :: MATRIX_1:37
for n, m, i, j being Nat
for D being non empty set
for M being Matrix of n,m,D st 1 <= i &amp; i <= n &amp; 1 <= j &amp; j <= m holds
[i,j] in Indices M
proofend;

:: from GOBOARD5, 2008.03.08, A.T.
theorem Th38: :: MATRIX_1:38
for M being tabular FinSequence
for i, j being Nat st [i,j] in Indices M holds
( 1 <= i &amp; i <= len M &amp; 1 <= j &amp; j <= width M )
proofend;

theorem :: MATRIX_1:39
for n, m, i, j being Nat
for D being non empty set
for M being Matrix of n,m,D st [i,j] in Indices M holds
( 1 <= i &amp; i <= n &amp; 1 <= j &amp; j <= m )
proofend;

:: from GOBRD13, 2011.07.26, A.T.
definition
let F be Function;
func Values F ->  set  equals :: MATRIX_1:def 16
 Union (rngs F);
correctness
coherence
Union (rngs F) is set ;
;
end;

:: deftheorem  defines Values MATRIX_1:def_16_:_
 for F being Function holds Values F = Union (rngs F);

theorem Th40: :: MATRIX_1:40
for i being Nat
for D being non empty set
for M being FinSequence of D * holds M . i is FinSequence of D
proofend;

theorem Th41: :: MATRIX_1:41
for D being non empty set
for M being FinSequence of D * holds Values M = union  {  (rng f) where f is Element of D * : f in rng M  }
proofend;

registration
let D be non empty set ;
let M be FinSequence of D * ;
cluster Values M ->  finite ;
coherence
 Values M is finite
proofend;
end;

theorem Th42: :: MATRIX_1:42
for i being Nat
for D being non empty set
for f being FinSequence of D
for M being Matrix of D st i in dom M &amp; M . i = f holds
len f = width M
proofend;

theorem Th43: :: MATRIX_1:43
for i, j being Nat
for D being non empty set
for f being FinSequence of D
for M being Matrix of D st i in dom M &amp; M . i = f &amp; j in dom f holds
[i,j] in Indices M
proofend;

theorem Th44: :: MATRIX_1:44
for i, j being Nat
for D being non empty set
for f being FinSequence of D
for M being Matrix of D st [i,j] in Indices M &amp; M . i = f holds
( len f = width M &amp; j in dom f )
proofend;

theorem Th45: :: MATRIX_1:45
for D being non empty set
for M being Matrix of D holds Values M =  {  (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M  }
proofend;

theorem :: MATRIX_1:46
for D being non empty set
for M being Matrix of D holds card (Values M) <= (len M) * (width M)
proofend;

theorem :: MATRIX_1:47
for D being non empty set
for i, j being Element of NAT
for M being Matrix of D st 1 <= i &amp; i <= len M &amp; 1 <= j &amp; j <= width M holds
M * (i,j) in Values M
proofend;