:: MATRIX_1 semantic presentation

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
proof
take M = {} ; ::_thesis: M is tabular
take  0 ; :: according to MATRIX_1:def_1 ::_thesis: for x being set st x in rng M holds
ex s being FinSequence st
( s = x & len s = 0 )
let x be set ; ::_thesis: ( x in rng M implies ex s being FinSequence st
( s = x & len s = 0 ) )
assume  x in rng M ; ::_thesis: ex s being FinSequence st
( s = x & len s = 0 )
hence  ex s being FinSequence st
( s = x & len s = 0 ) ; ::_thesis: verum
end;
end;

theorem Th1: :: MATRIX_1:1
for D being non empty set
for d being Element of D holds <*<*d*>*> is tabular
proof
let D be non empty set ; ::_thesis: for d being Element of D holds <*<*d*>*> is tabular
let d be Element of D; ::_thesis: <*<*d*>*> is tabular
take n = 1; :: according to MATRIX_1:def_1 ::_thesis: for x being set st x in rng <*<*d*>*> holds
ex s being FinSequence st
( s = x & len s = n )
let x be set ; ::_thesis: ( x in rng <*<*d*>*> implies ex s being FinSequence st
( s = x & len s = n ) )
assume A1: x in rng <*<*d*>*> ; ::_thesis: ex s being FinSequence st
( s = x & len s = n )
A2: len <*d*> = n by FINSEQ_1:39;
 rng <*<*d*>*> = {<*d*>} by FINSEQ_1:38;
then  x = <*d*> by A1, TARSKI:def_1;
hence  ex s being FinSequence st
( s = x & len s = n ) by A2; ::_thesis: verum
end;

theorem Th2: :: MATRIX_1:2
for x being set
for m, n being Nat holds m |-> (n |-> x) is tabular
proof
let x be set ; ::_thesis: for m, n being Nat holds m |-> (n |-> x) is tabular
let m, n be Nat; ::_thesis: m |-> (n |-> x) is tabular
set s = m |-> (n |-> x);
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
take  n1 ; :: according to MATRIX_1:def_1 ::_thesis: for x being set st x in rng (m |-> (n |-> x)) holds
ex s being FinSequence st
( s = x & len s = n1 )
let z be set ; ::_thesis: ( z in rng (m |-> (n |-> x)) implies ex s being FinSequence st
( s = z & len s = n1 ) )
assume A1: z in rng (m |-> (n |-> x)) ; ::_thesis: ex s being FinSequence st
( s = z & len s = n1 )
take  n |-> x ; ::_thesis: ( n |-> x = z & len (n |-> x) = n1 )
 rng (m |-> (n |-> x)) c= {(n |-> x)} by FUNCOP_1:13;
hence  ( n |-> x = z & len (n |-> x) = n1 ) by A1, CARD_1:def_7, TARSKI:def_1; ::_thesis: verum
end;

theorem Th3: :: MATRIX_1:3
for s being FinSequence holds <*s*> is tabular
proof
let s be FinSequence; ::_thesis: <*s*> is tabular
take  len s ; :: according to MATRIX_1:def_1 ::_thesis: for x being set st x in rng <*s*> holds
ex s being FinSequence st
( s = x & len s = len s )
let x be set ; ::_thesis: ( x in rng <*s*> implies ex s being FinSequence st
( s = x & len s = len s ) )
assume  x in rng <*s*> ; ::_thesis: ex s being FinSequence st
( s = x & len s = len s )
then A1: x in {s} by FINSEQ_1:38;
then reconsider t = x as FinSequence by TARSKI:def_1;
take  t ; ::_thesis: ( t = x & len t = len s )
thus  ( t = x & len t = len s ) by A1, TARSKI:def_1; ::_thesis: verum
end;

theorem Th4: :: MATRIX_1:4
for n being Nat
for s1, s2 being FinSequence st len s1 = n & len s2 = n holds
<*s1,s2*> is tabular
proof
let n be Nat; ::_thesis: for s1, s2 being FinSequence st len s1 = n & len s2 = n holds
<*s1,s2*> is tabular
let s1, s2 be FinSequence; ::_thesis: ( len s1 = n & len s2 = n implies <*s1,s2*> is tabular )
assume A1: ( len s1 = n & len s2 = n ) ; ::_thesis: <*s1,s2*> is tabular
now__::_thesis:_ex_n_being_Nat_st_
for_x_being_set_st_x_in_rng_<*s1,s2*>_holds_
ex_r_being_FinSequence_st_
(_x_=_r_&_len_r_=_n_)
take n = n; ::_thesis: for x being set st x in rng <*s1,s2*> holds
ex r being FinSequence st
( x = r & len r = n )
let x be set ; ::_thesis: ( x in rng <*s1,s2*> implies ex r being FinSequence st
( x = r & len r = n ) )
assume  x in rng <*s1,s2*> ; ::_thesis: ex r being FinSequence st
( x = r & len r = n )
then A2: x in {s1,s2} by FINSEQ_2:127;
then reconsider r = x as FinSequence by TARSKI:def_2;
take r = r; ::_thesis: ( x = r & len r = n )
thus  ( x = r & len r = n ) by A1, A2, TARSKI:def_2; ::_thesis: verum
end;
hence  <*s1,s2*> is tabular by Def1; ::_thesis: verum
end;

theorem Th5: :: MATRIX_1:5
{} is tabular
proof
now__::_thesis:_ex_n_being_set_st_
for_x_being_set_st_x_in_rng_{}_holds_
ex_t_being_FinSequence_st_
(_t_=_x_&_len_t_=_n_)
take n = 0 ; ::_thesis: for x being set st x in rng {} holds
ex t being FinSequence st
( t = x & len t = n )
let x be set ; ::_thesis: ( x in rng {} implies ex t being FinSequence st
( t = x & len t = n ) )
assume  x in rng {} ; ::_thesis: ex t being FinSequence st
( t = x & len t = n )
hence  ex t being FinSequence st
( t = x & len t = n ) ; ::_thesis: verum
end;
hence  {} is tabular by Def1; ::_thesis: verum
end;

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
proof
let D be non empty set ; ::_thesis: for a1, a2 being Element of D holds <*<*a1*>,<*a2*>*> is tabular
let a1, a2 be Element of D; ::_thesis: <*<*a1*>,<*a2*>*> is tabular
 ( len <*a1*> = 1 & len <*a2*> = 1 ) by FINSEQ_1:39;
hence  <*<*a1*>,<*a2*>*> is tabular by Th4; ::_thesis: verum
end;

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
proof
let D be non empty set ; ::_thesis: for a1, a2, b1, b2 being Element of D holds <*<*a1,a2*>,<*b1,b2*>*> is tabular
let a1, a2, b1, b2 be Element of D; ::_thesis: <*<*a1,a2*>,<*b1,b2*>*> is tabular
 ( len <*a1,a2*> = 2 & len <*b1,b2*> = 2 ) by FINSEQ_1:44;
hence  <*<*a1,a2*>,<*b1,b2*>*> is tabular by Th4; ::_thesis: verum
end;

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
proof
take  <*> (D *) ; ::_thesis: <*> (D *) is tabular
take  0 ; :: according to MATRIX_1:def_1 ::_thesis: for x being set st x in rng (<*> (D *)) holds
ex s being FinSequence st
( s = x & len s = 0 )
thus  for x being set st x in rng (<*> (D *)) holds
ex s being FinSequence st
( s = x & len s = 0 ) ; ::_thesis: verum
end;
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
proof
set d = the Element of D;
A1: rng <*<* the Element of D*>*> = {<* the Element of D*>} by FINSEQ_1:38;
 <* the Element of D*> in D * by FINSEQ_1:def_11;
then  rng <*<* the Element of D*>*> c= D * by A1, ZFMISC_1:31;
then reconsider p = <*<* the Element of D*>*> as FinSequence of D * by FINSEQ_1:def_4;
reconsider s = <* the Element of D*> as FinSequence ;
reconsider p = p as tabular FinSequence of D * by Th1;
take  p ; ::_thesis: not p is empty-yielding
now__::_thesis:_ex_s_being_FinSequence_st_
(_s_in_rng_p_&_s_<>_{}_)
take s = s; ::_thesis: ( s in rng p & s <> {} )
thus  s in rng p by A1, TARSKI:def_1; ::_thesis: s <> {}
thus  s <> {} ; ::_thesis: verum
end;
hence  not p is empty-yielding by RELAT_1:149; ::_thesis: verum
end;
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 & len p = n ) )
proof
let D be non empty set ; ::_thesis: 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 & len p = n ) )
let s be FinSequence; ::_thesis: ( 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 & len p = n ) )
thus  ( s is Matrix of D implies ex n being Nat st
for x being set st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n ) ) ::_thesis: ( ex n being Nat st
for x being set st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n ) implies s is Matrix of D )
proof
assume  s is Matrix of D ; ::_thesis: ex n being Nat st
for x being set st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n )
then reconsider s = s as tabular FinSequence of D * ;
consider n being Nat such that
A1: for x being set st x in rng s holds
ex t being FinSequence st
( t = x & len t = n ) by Def1;
take  n ; ::_thesis: for x being set st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n )
 for x being set st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n )
proof
let x be set ; ::_thesis: ( x in rng s implies ex p being FinSequence of D st
( x = p & len p = n ) )
assume A2: x in rng s ; ::_thesis: ex p being FinSequence of D st
( x = p & len p = n )
then consider v being FinSequence such that
A3: v = x and
A4: len v = n by A1;
 rng s c= D * by FINSEQ_1:def_4;
then reconsider p = v as FinSequence of D by A2, A3, FINSEQ_1:def_11;
take  p ; ::_thesis: ( x = p & len p = n )
thus  ( x = p & len p = n ) by A3, A4; ::_thesis: verum
end;
hence  for x being set st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n ) ; ::_thesis: verum
end;
given n being Nat such that A5: for x being set st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n ) ; ::_thesis: s is Matrix of D
A6: s is tabular
proof
consider n being Nat such that
A7: for x being set st x in rng s holds
ex p being FinSequence of D st
( x = p & len p = n ) by A5;
take  n ; :: according to MATRIX_1:def_1 ::_thesis: for x being set st x in rng s holds
ex s being FinSequence st
( s = x & len s = n )
 for x being set st x in rng s holds
ex t being FinSequence st
( t = x & len t = n )
proof
let x be set ; ::_thesis: ( x in rng s implies ex t being FinSequence st
( t = x & len t = n ) )
assume  x in rng s ; ::_thesis: ex t being FinSequence st
( t = x & len t = n )
then consider p being FinSequence of D such that
A8: ( x = p & len p = n ) by A7;
reconsider t = p as FinSequence ;
take  t ; ::_thesis: ( t = x & len t = n )
thus  ( t = x & len t = n ) by A8; ::_thesis: verum
end;
hence  for x being set st x in rng s holds
ex s being FinSequence st
( s = x & len s = n ) ; ::_thesis: verum
end;
 rng s c= D *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng s or x in D * )
assume  x in rng s ; ::_thesis: x in D *
then  ex p being FinSequence of D st
( x = p & len p = n ) by A5;
then reconsider q = x as FinSequence of D ;
 q in D * by FINSEQ_1:def_11;
hence  x in D * ; ::_thesis: verum
end;
hence  s is Matrix of D by A6, FINSEQ_1:def_4; ::_thesis: verum
end;

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 & ( 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 & ( for p being FinSequence of D st p in rng b1 holds
len p = n ) )
proof
reconsider m1 = m, n1 = n as Element of NAT by ORDINAL1:def_12;
set a = the Element of D;
reconsider d = n1 |-> the Element of D as Element of D * by FINSEQ_1:def_11;
reconsider M = m1 |-> d as FinSequence of D * ;
 ex n being Element of NAT st
for x being set st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = n )
proof
reconsider p = n1 |-> the Element of D as FinSequence of D ;
take  n1 ; ::_thesis: for x being set st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = n1 )
let x be set ; ::_thesis: ( x in rng M implies ex p being FinSequence of D st
( x = p & len p = n1 ) )
assume A1: x in rng M ; ::_thesis: ex p being FinSequence of D st
( x = p & len p = n1 )
take  p ; ::_thesis: ( x = p & len p = n1 )
 rng M c= {(n |-> the Element of D)} by FUNCOP_1:13;
hence  ( x = p & len p = n1 ) by A1, CARD_1:def_7, TARSKI:def_1; ::_thesis: verum
end;
then reconsider M = M as Matrix of D by Th9;
take  M ; ::_thesis: ( len M = m & ( for p being FinSequence of D st p in rng M holds
len p = n ) )
thus  len M = m by CARD_1:def_7; ::_thesis: for p being FinSequence of D st p in rng M holds
len p = n
let p be FinSequence of D; ::_thesis: ( p in rng M implies len p = n )
A2: rng M c= {(n |-> the Element of D)} by FUNCOP_1:13;
assume  p in rng M ; ::_thesis: len p = n
then  p = n |-> the Element of D by A2, TARSKI:def_1;
hence  len p = n by CARD_1:def_7; ::_thesis: verum
end;
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 & ( 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
proof
let m, n be Nat; ::_thesis: for D being non empty set
for a being Element of D holds m |-> (n |-> a) is Matrix of m,n,D
let D be non empty set ; ::_thesis: for a being Element of D holds m |-> (n |-> a) is Matrix of m,n,D
let a be Element of D; ::_thesis: m |-> (n |-> a) is Matrix of m,n,D
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def_12;
reconsider d = n1 |-> a as Element of D * by FINSEQ_1:def_11;
reconsider M = m1 |-> d as FinSequence of D * ;
reconsider M = M as Matrix of D by Th2;
 M is Matrix of m,n,D
proof
thus  len M = m by CARD_1:def_7; :: according to MATRIX_1:def_2 ::_thesis: for p being FinSequence of D st p in rng M holds
len p = n
let p be FinSequence of D; ::_thesis: ( p in rng M implies len p = n )
A1: rng M c= {(n |-> a)} by FUNCOP_1:13;
assume  p in rng M ; ::_thesis: len p = n
then  p = n |-> a by A1, TARSKI:def_1;
hence  len p = n by CARD_1:def_7; ::_thesis: verum
end;
hence  m |-> (n |-> a) is Matrix of m,n,D ; ::_thesis: verum
end;

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
proof
let D be non empty set ; ::_thesis: for p being FinSequence of D holds <*p*> is Matrix of 1, len p,D
let p be FinSequence of D; ::_thesis: <*p*> is Matrix of 1, len p,D
reconsider p9 = p as Element of D * by FINSEQ_1:def_11;
 <*p9*> is tabular by Th3;
then reconsider M = <*p*> as Matrix of D ;
 M is Matrix of 1, len p,D
proof
thus  len M = 1 by FINSEQ_1:39; :: according to MATRIX_1:def_2 ::_thesis: for p being FinSequence of D st p in rng M holds
len p = len p
let q be FinSequence of D; ::_thesis: ( q in rng M implies len q = len p )
assume  q in rng M ; ::_thesis: len q = len p
then  q in {p} by FINSEQ_1:38;
hence  len q = len p by TARSKI:def_1; ::_thesis: verum
end;
hence  <*p*> is Matrix of 1, len p,D ; ::_thesis: verum
end;

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 & len p2 = n holds
<*p1,p2*> is Matrix of 2,n,D
proof
let n be Nat; ::_thesis: for D being non empty set
for p1, p2 being FinSequence of D st len p1 = n & len p2 = n holds
<*p1,p2*> is Matrix of 2,n,D
let D be non empty set ; ::_thesis: for p1, p2 being FinSequence of D st len p1 = n & len p2 = n holds
<*p1,p2*> is Matrix of 2,n,D
let p1, p2 be FinSequence of D; ::_thesis: ( len p1 = n & len p2 = n implies <*p1,p2*> is Matrix of 2,n,D )
reconsider q1 = p1, q2 = p2 as Element of D * by FINSEQ_1:def_11;
reconsider M = <*q1,q2*> as FinSequence of D * by FINSEQ_2:13;
assume A1: ( len p1 = n & len p2 = n ) ; ::_thesis: <*p1,p2*> is Matrix of 2,n,D
then reconsider M = M as Matrix of D by Th4;
 M is Matrix of 2,n,D
proof
thus  len M = 2 by FINSEQ_1:44; :: according to MATRIX_1:def_2 ::_thesis: for p being FinSequence of D st p in rng M holds
len p = n
let r be FinSequence of D; ::_thesis: ( r in rng M implies len r = n )
assume  r in rng M ; ::_thesis: len r = n
then  r in {p1,p2} by FINSEQ_2:127;
hence  len r = n by A1, TARSKI:def_2; ::_thesis: verum
end;
hence  <*p1,p2*> is Matrix of 2,n,D ; ::_thesis: verum
end;

theorem Th13: :: MATRIX_1:13
for m being Nat
for D being non empty set holds {} is Matrix of 0 ,m,D
proof
let m be Nat; ::_thesis: for D being non empty set holds {} is Matrix of 0 ,m,D
let D be non empty set ; ::_thesis: {} is Matrix of 0 ,m,D
reconsider M = <*> (D *) as FinSequence of D * ;
reconsider M = M as Matrix of D by Th5;
 M is Matrix of 0 ,m,D
proof
thus  len M = 0 ; :: according to MATRIX_1:def_2 ::_thesis: for p being FinSequence of D st p in rng M holds
len p = m
let p be FinSequence of D; ::_thesis: ( p in rng M implies len p = m )
assume  p in rng M ; ::_thesis: len p = m
hence  len p = m ; ::_thesis: verum
end;
hence  {} is Matrix of 0 ,m,D ; ::_thesis: verum
end;

theorem :: MATRIX_1:14
for D being non empty set holds <*{}*> is Matrix of 1, 0 ,D
proof
let D be non empty set ; ::_thesis: <*{}*> is Matrix of 1, 0 ,D
 len (<*> D) = 0 ;
hence  <*{}*> is Matrix of 1, 0 ,D by Th11; ::_thesis: verum
end;

theorem :: MATRIX_1:15
for D being non empty set
for a being Element of D holds <*<*a*>*> is Matrix of 1,D
proof
let D be non empty set ; ::_thesis: for a being Element of D holds <*<*a*>*> is Matrix of 1,D
let a be Element of D; ::_thesis: <*<*a*>*> is Matrix of 1,D
 len <*a*> = 1 by FINSEQ_1:39;
hence  <*<*a*>*> is Matrix of 1,D by Th11; ::_thesis: verum
end;

theorem :: MATRIX_1:16
for D being non empty set holds <*{},{}*> is Matrix of 2, 0 ,D
proof
let D be non empty set ; ::_thesis: <*{},{}*> is Matrix of 2, 0 ,D
 len (<*> D) = 0 ;
hence  <*{},{}*> is Matrix of 2, 0 ,D by Th12; ::_thesis: verum
end;

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
proof
let D be non empty set ; ::_thesis: for a1, a2 being Element of D holds <*<*a1,a2*>*> is Matrix of 1,2,D
let a1, a2 be Element of D; ::_thesis: <*<*a1,a2*>*> is Matrix of 1,2,D
 ( <*a1,a2*> is FinSequence of D & len <*a1,a2*> = 2 ) by FINSEQ_1:44, FINSEQ_2:13;
hence  <*<*a1,a2*>*> is Matrix of 1,2,D by Th11; ::_thesis: verum
end;

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
proof
let D be non empty set ; ::_thesis: for a1, a2 being Element of D holds <*<*a1*>,<*a2*>*> is Matrix of 2,1,D
let a1, a2 be Element of D; ::_thesis: <*<*a1*>,<*a2*>*> is Matrix of 2,1,D
 ( len <*a1*> = 1 & len <*a2*> = 1 ) by FINSEQ_1:39;
hence  <*<*a1*>,<*a2*>*> is Matrix of 2,1,D by Th12; ::_thesis: verum
end;

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
proof
let D be non empty set ; ::_thesis: for a1, a2, b1, b2 being Element of D holds <*<*a1,a2*>,<*b1,b2*>*> is Matrix of 2,D
let a1, a2, b1, b2 be Element of D; ::_thesis: <*<*a1,a2*>,<*b1,b2*>*> is Matrix of 2,D
A1: ( len <*a1,a2*> = 2 & len <*b1,b2*> = 2 ) by FINSEQ_1:44;
 ( <*a1,a2*> is FinSequence of D & <*b1,b2*> is FinSequence of D ) by FINSEQ_2:13;
hence  <*<*a1,a2*>,<*b1,b2*>*> is Matrix of 2,D by A1, Th12; ::_thesis: verum
end;


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 & 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 & len s = b1 ) ) & ( not len M > 0 implies ex b1 being Element of NAT st b1 = 0 ) )
proof
thus  ( len M > 0 implies ex n being Element of NAT ex s being FinSequence st
( s in rng M & len s = n ) ) ::_thesis: ( not len M > 0 implies ex b1 being Element of NAT st b1 = 0 )
proof
set x = the Element of rng M;
consider n being Nat such that
A1: for x being set st x in rng M holds
ex s being FinSequence st
( s = x & len s = n ) by Def1;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
assume  len M > 0 ; ::_thesis: ex n being Element of NAT ex s being FinSequence st
( s in rng M & len s = n )
then A2: rng M <> {} by CARD_1:27, RELAT_1:41;
then consider s being FinSequence such that
A3: ( s = the Element of rng M & len s = n ) by A1;
take  n ; ::_thesis: ex s being FinSequence st
( s in rng M & len s = n )
take  s ; ::_thesis: ( s in rng M & len s = n )
thus  ( s in rng M & len s = n ) by A2, A3; ::_thesis: verum
end;
 0 in NAT by ORDINAL1:def_12;
hence  ( not len M > 0 implies ex b1 being Element of NAT st b1 = 0 ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT holds
( ( len M > 0 & ex s being FinSequence st
( s in rng M & len s = b1 ) & ex s being FinSequence st
( s in rng M & len s = b2 ) implies b1 = b2 ) & ( not len M > 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof
let n1, n2 be Element of NAT ; ::_thesis: ( ( len M > 0 & ex s being FinSequence st
( s in rng M & len s = n1 ) & ex s being FinSequence st
( s in rng M & len s = n2 ) implies n1 = n2 ) & ( not len M > 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) )
thus  ( len M > 0 & ex s being FinSequence st
( s in rng M & len s = n1 ) & ex s being FinSequence st
( s in rng M & len s = n2 ) implies n1 = n2 ) ::_thesis: ( not len M > 0 & n1 = 0 & n2 = 0 implies n1 = n2 )
proof
assume  len M > 0 ; ::_thesis: ( for s being FinSequence holds
( not s in rng M or not len s = n1 ) or for s being FinSequence holds
( not s in rng M or not len s = n2 ) or n1 = n2 )
given s being FinSequence such that A4: s in rng M and
A5: len s = n1 ; ::_thesis: ( for s being FinSequence holds
( not s in rng M or not len s = n2 ) or n1 = n2 )
consider n being Nat such that
A6: for x being set st x in rng M holds
ex s being FinSequence st
( s = x & len s = n ) by Def1;
A7: ex s1 being FinSequence st
( s1 = s & len s1 = n ) by A6, A4;
given p being FinSequence such that A8: p in rng M and
A9: len p = n2 ; ::_thesis: n1 = n2
 ex p1 being FinSequence st
( p1 = p & len p1 = n ) by A6, A8;
hence  n1 = n2 by A5, A9, A7; ::_thesis: verum
end;
thus  ( not len M > 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) ; ::_thesis: verum
end;
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 & len s = b2 ) ) ) & ( 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 )
proof
let D be non empty set ; ::_thesis: 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 )
let M be Matrix of D; ::_thesis: ( len M > 0 implies for n being Nat holds
( M is Matrix of len M,n,D iff n = width M ) )
assume A1: len M > 0 ; ::_thesis: for n being Nat holds
( M is Matrix of len M,n,D iff n = width M )
let n be Nat; ::_thesis: ( M is Matrix of len M,n,D iff n = width M )
thus  ( M is Matrix of len M,n,D implies n = width M ) ::_thesis: ( n = width M implies M is Matrix of len M,n,D )
proof
consider s being FinSequence such that
A2: s in rng M and
A3: len s = width M by A1, Def3;
 rng M c= D * by FINSEQ_1:def_4;
then reconsider q = s as FinSequence of D by A2, FINSEQ_1:def_11;
assume  M is Matrix of len M,n,D ; ::_thesis: n = width M
then  len q = n by A2, Def2;
hence  n = width M by A3; ::_thesis: verum
end;
assume  n = width M ; ::_thesis: M is Matrix of len M,n,D
then  for p being FinSequence of D st p in rng M holds
len p = n by A1, Def3;
hence  M is Matrix of len M,n,D by Def2; ::_thesis: verum
end;

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 & it = p . j );
existence
 ex b1 being Element of D ex p being FinSequence of D st
( p = M . i & b1 = p . j )
proof
 i in dom M by A1, ZFMISC_1:87;
then A2: M . i in rng M by FUNCT_1:def_3;
 rng M c= D * by FINSEQ_1:def_4;
then reconsider p = M . i as FinSequence of D by A2, FINSEQ_1:def_11;
A3: j in Seg (width M) by A1, ZFMISC_1:87;
 ( M <> {} & len M >= 0 ) by A1, NAT_1:2, ZFMISC_1:87;
then  len M > 0 by XXREAL_0:1;
then consider s being FinSequence such that
A4: s in rng M and
A5: len s = width M by Def3;
consider n being Nat such that
A6: for x being set st x in rng M holds
ex t being FinSequence st
( t = x & len t = n ) by Def1;
A7: ex v being FinSequence st
( p = v & len v = n ) by A2, A6;
 ex t being FinSequence st
( s = t & len t = n ) by A4, A6;
then  j in dom p by A3, A5, A7, FINSEQ_1:def_3;
then A8: p . j in rng p by FUNCT_1:def_3;
 rng p c= D by FINSEQ_1:def_4;
then reconsider a = p . j as Element of D by A8;
take  a ; ::_thesis: ex p being FinSequence of D st
( p = M . i & a = p . j )
take  p ; ::_thesis: ( p = M . i & a = p . j )
thus  ( p = M . i & a = p . j ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of D st ex p being FinSequence of D st
( p = M . i & b1 = p . j ) & ex p being FinSequence of D st
( p = M . i & 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 & 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 & width M1 = width M2 & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) ) holds
M1 = M2
proof
let D be non empty set ; ::_thesis: for M1, M2 being Matrix of D st len M1 = len M2 & width M1 = width M2 & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) ) holds
M1 = M2
let M1, M2 be Matrix of D; ::_thesis: ( len M1 = len M2 & width M1 = width M2 & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) ) implies M1 = M2 )
assume that
A1: len M1 = len M2 and
A2: width M1 = width M2 and
A3: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) ; ::_thesis: M1 = M2
A4: dom M1 = dom M2 by A1, FINSEQ_3:29;
 for k being Nat st k in dom M1 holds
M1 . k = M2 . k
proof
let k be Nat; ::_thesis: ( k in dom M1 implies M1 . k = M2 . k )
A5: len M1 >= 0 by NAT_1:2;
assume A6: k in dom M1 ; ::_thesis: M1 . k = M2 . k
then A7: M1 . k in rng M1 by FUNCT_1:def_3;
 rng M1 c= D * by FINSEQ_1:def_4;
then reconsider p = M1 . k as FinSequence of D by A7, FINSEQ_1:def_11;
 M1 <> {} by A6;
then A8: len M1 > 0 by A5, XXREAL_0:1;
then  M1 is Matrix of len M1, width M1,D by Th20;
then A9: len p = width M1 by A7, Def2;
A10: M2 . k in rng M2 by A4, A6, FUNCT_1:def_3;
 rng M2 c= D * by FINSEQ_1:def_4;
then reconsider q = M2 . k as FinSequence of D by A10, FINSEQ_1:def_11;
 M2 is Matrix of len M1, width M1,D by A1, A2, A8, Th20;
then A11: len q = width M1 by A10, Def2;
 for l being Nat st 1 <= l & l <= len p holds
p . l = q . l
proof
let l be Nat; ::_thesis: ( 1 <= l & l <= len p implies p . l = q . l )
A12: rng p c= D by FINSEQ_1:def_4;
assume  ( 1 <= l & l <= len p ) ; ::_thesis: p . l = q . l
then A13: l in Seg (width M1) by A9, FINSEQ_1:1;
then  l in dom p by A9, FINSEQ_1:def_3;
then  p . l in rng p by FUNCT_1:def_3;
then reconsider a = p . l as Element of D by A12;
A14: rng q c= D by FINSEQ_1:def_4;
 l in dom q by A11, A13, FINSEQ_1:def_3;
then  q . l in rng q by FUNCT_1:def_3;
then reconsider b = q . l as Element of D by A14;
 [k,l] in Indices M2 by A2, A4, A6, A13, ZFMISC_1:87;
then A15: M2 * (k,l) = b by Def5;
 [k,l] in Indices M1 by A6, A13, ZFMISC_1:87;
then A16: M1 * (k,l) = a by Def5;
 [k,l] in [:(dom M1),(Seg (width M1)):] by A6, A13, ZFMISC_1:87;
hence  p . l = q . l by A3, A16, A15; ::_thesis: verum
end;
hence  M1 . k = M2 . k by A9, A11, FINSEQ_1:14; ::_thesis: verum
end;
hence  M1 = M2 by A4, FINSEQ_1:13; ::_thesis: verum
end;

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)
proof
defpred S1[ set , set ] means  ex p being FinSequence st
( $2 = p & len p = F3() & ( for i being Nat st i in Seg F3() holds
p . i = F4($1,i) ) );
A1: F2() >= 0 by NAT_1:2;
A2: for k being Nat st k in Seg F2() holds
ex y being set st S1[k,y]
proof
let k be Nat; ::_thesis: ( k in Seg F2() implies ex y being set st S1[k,y] )
assume  k in Seg F2() ; ::_thesis: ex y being set st S1[k,y]
deffunc H1( Nat) ->  Element of F1() = F4(k,$1);
consider p being FinSequence such that
A3: ( len p = F3() & ( for i being Nat st i in dom p holds
p . i = H1(i) ) ) from FINSEQ_1:sch_2();
take  p ; ::_thesis: S1[k,p]
take  p ; ::_thesis: ( p = p & len p = F3() & ( for i being Nat st i in Seg F3() holds
p . i = F4(k,i) ) )
 dom p = Seg F3() by A3, FINSEQ_1:def_3;
hence  ( p = p & len p = F3() & ( for i being Nat st i in Seg F3() holds
p . i = F4(k,i) ) ) by A3; ::_thesis: verum
end;
consider M being FinSequence such that
A4: dom M = Seg F2() and
A5: for k being Nat st k in Seg F2() holds
S1[k,M . k] from FINSEQ_1:sch_1(A2);
A6: len M = F2() by A4, FINSEQ_1:def_3;
 rng M c= F1() *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng M or x in F1() * )
assume  x in rng M ; ::_thesis: x in F1() *
then consider i being Nat such that
A7: i in dom M and
A8: M . i = x by FINSEQ_2:10;
consider p being FinSequence such that
A9: M . i = p and
A10: ( len p = F3() & ( for j being Nat st j in Seg F3() holds
p . j = F4(i,j) ) ) by A4, A5, A7;
 rng p c= F1()
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng p or z in F1() )
assume  z in rng p ; ::_thesis: z in F1()
then consider k being Nat such that
A11: k in dom p and
A12: p . k = z by FINSEQ_2:10;
 k in Seg (len p) by A11, FINSEQ_1:def_3;
then  z = F4(i,k) by A10, A12;
hence  z in F1() ; ::_thesis: verum
end;
then  p is FinSequence of F1() by FINSEQ_1:def_4;
hence  x in F1() * by A8, A9, FINSEQ_1:def_11; ::_thesis: verum
end;
then reconsider M = M as FinSequence of F1() * by FINSEQ_1:def_4;
 ex n being Nat st
for x being set st x in rng M holds
ex p being FinSequence of F1() st
( x = p & len p = n )
proof
take  F3() ; ::_thesis: for x being set st x in rng M holds
ex p being FinSequence of F1() st
( x = p & len p = F3() )
let x be set ; ::_thesis: ( x in rng M implies ex p being FinSequence of F1() st
( x = p & len p = F3() ) )
assume  x in rng M ; ::_thesis: ex p being FinSequence of F1() st
( x = p & len p = F3() )
then consider i being Nat such that
A13: ( i in dom M & M . i = x ) by FINSEQ_2:10;
consider p being FinSequence such that
A14: x = p and
A15: len p = F3() and
A16: for j being Nat st j in Seg F3() holds
p . j = F4(i,j) by A4, A5, A13;
 rng p c= F1()
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng p or z in F1() )
assume  z in rng p ; ::_thesis: z in F1()
then consider k being Nat such that
A17: k in dom p and
A18: p . k = z by FINSEQ_2:10;
 k in Seg (len p) by A17, FINSEQ_1:def_3;
then  z = F4(i,k) by A15, A16, A18;
hence  z in F1() ; ::_thesis: verum
end;
then reconsider p = p as FinSequence of F1() by FINSEQ_1:def_4;
take  p ; ::_thesis: ( x = p & len p = F3() )
thus  ( x = p & len p = F3() ) by A14, A15; ::_thesis: verum
end;
then reconsider M = M as Matrix of F1() by Th9;
 for p being FinSequence of F1() st p in rng M holds
len p = F3()
proof
let p be FinSequence of F1(); ::_thesis: ( p in rng M implies len p = F3() )
assume  p in rng M ; ::_thesis: len p = F3()
then consider i being Nat such that
A19: ( i in dom M & M . i = p ) by FINSEQ_2:10;
 S1[i,p] by A4, A5, A19;
hence  len p = F3() ; ::_thesis: verum
end;
then reconsider M = M as Matrix of F2(),F3(),F1() by A6, Def2;
take  M ; ::_thesis: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = F4(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices M implies M * (i,j) = F4(i,j) )
assume A20: [i,j] in Indices M ; ::_thesis: M * (i,j) = F4(i,j)
then  F2() <> 0 by A4, ZFMISC_1:87;
then A21: F2() > 0 by A1, XXREAL_0:1;
 i in Seg F2() by A4, A20, ZFMISC_1:87;
then A22: ex q being FinSequence st
( M . i = q & len q = F3() & ( for j being Nat st j in Seg F3() holds
q . j = F4(i,j) ) ) by A5;
 j in Seg (width M) by A20, ZFMISC_1:87;
then A23: j in Seg F3() by A6, A21, Th20;
 ex p being FinSequence of F1() st
( p = M . i & M * (i,j) = p . j ) by A20, Def5;
hence  M * (i,j) = F4(i,j) by A22, A23; ::_thesis: verum
end;

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]
proof
defpred S1[ set , set , set ] means ( P1[$1,$2,$3] & $3 in F1() );
A2: for x, y being set st x in Seg F2() & y in Seg F3() holds
ex z being set st
( z in F1() & S1[x,y,z] )
proof
let x, y be set ; ::_thesis: ( x in Seg F2() & y in Seg F3() implies ex z being set st
( z in F1() & S1[x,y,z] ) )
assume that
A3: x in Seg F2() and
A4: y in Seg F3() ; ::_thesis: ex z being set st
( z in F1() & S1[x,y,z] )
reconsider y9 = y as Element of NAT by A4;
reconsider x9 = x as Element of NAT by A3;
 [x9,y9] in [:(Seg F2()),(Seg F3()):] by A3, A4, ZFMISC_1:87;
then consider z9 being Element of F1() such that
A5: P1[x9,y9,z9] by A1;
take  z9 ; ::_thesis: ( z9 in F1() & S1[x,y,z9] )
thus  ( z9 in F1() & S1[x,y,z9] ) by A5; ::_thesis: verum
end;
consider f being Function of [:(Seg F2()),(Seg F3()):],F1() such that
A6: for x, y being set st x in Seg F2() & y in Seg F3() holds
S1[x,y,f . (x,y)] from BINOP_1:sch_1(A2);
A7: F2() >= 0 by NAT_1:2;
defpred S2[ set , set ] means  ex p being FinSequence st
( $2 = p & len p = F3() & ( for i being Nat st i in Seg F3() holds
p . i = f . ($1,i) ) );
A8: for k being Nat st k in Seg F2() holds
ex y being set st S2[k,y]
proof
let k be Nat; ::_thesis: ( k in Seg F2() implies ex y being set st S2[k,y] )
assume  k in Seg F2() ; ::_thesis: ex y being set st S2[k,y]
deffunc H1( Nat) ->  set = f . [k,$1];
consider p being FinSequence such that
A9: ( len p = F3() & ( for i being Nat st i in dom p holds
p . i = H1(i) ) ) from FINSEQ_1:sch_2();
take  p ; ::_thesis: S2[k,p]
take  p ; ::_thesis: ( p = p & len p = F3() & ( for i being Nat st i in Seg F3() holds
p . i = f . (k,i) ) )
 dom p = Seg F3() by A9, FINSEQ_1:def_3;
hence  ( p = p & len p = F3() & ( for i being Nat st i in Seg F3() holds
p . i = f . (k,i) ) ) by A9; ::_thesis: verum
end;
consider M being FinSequence such that
A10: dom M = Seg F2() and
A11: for k being Nat st k in Seg F2() holds
S2[k,M . k] from FINSEQ_1:sch_1(A8);
A12: len M = F2() by A10, FINSEQ_1:def_3;
 rng M c= F1() *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng M or x in F1() * )
assume  x in rng M ; ::_thesis: x in F1() *
then consider i being Nat such that
A13: i in Seg F2() and
A14: M . i = x by A10, FINSEQ_2:10;
consider p being FinSequence such that
A15: M . i = p and
A16: len p = F3() and
A17: for j being Nat st j in Seg F3() holds
p . j = f . (i,j) by A11, A13;
 rng p c= F1()
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng p or z in F1() )
assume  z in rng p ; ::_thesis: z in F1()
then consider k being Nat such that
A18: k in dom p and
A19: p . k = z by FINSEQ_2:10;
A20: k in Seg (len p) by A18, FINSEQ_1:def_3;
then A21: [i,k] in [:(Seg F2()),(Seg F3()):] by A13, A16, ZFMISC_1:87;
 z = f . (i,k) by A16, A17, A19, A20;
hence  z in F1() by A21, FUNCT_2:5; ::_thesis: verum
end;
then  p is FinSequence of F1() by FINSEQ_1:def_4;
hence  x in F1() * by A14, A15, FINSEQ_1:def_11; ::_thesis: verum
end;
then reconsider M = M as FinSequence of F1() * by FINSEQ_1:def_4;
 ex n being Nat st
for x being set st x in rng M holds
ex p being FinSequence of F1() st
( x = p & len p = n )
proof
take  F3() ; ::_thesis: for x being set st x in rng M holds
ex p being FinSequence of F1() st
( x = p & len p = F3() )
let x be set ; ::_thesis: ( x in rng M implies ex p being FinSequence of F1() st
( x = p & len p = F3() ) )
assume  x in rng M ; ::_thesis: ex p being FinSequence of F1() st
( x = p & len p = F3() )
then consider i being Nat such that
A22: i in dom M and
A23: M . i = x by FINSEQ_2:10;
consider p being FinSequence such that
A24: x = p and
A25: len p = F3() and
A26: for j being Nat st j in Seg F3() holds
p . j = f . (i,j) by A10, A11, A22, A23;
 rng p c= F1()
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng p or z in F1() )
assume  z in rng p ; ::_thesis: z in F1()
then consider k being Nat such that
A27: k in dom p and
A28: p . k = z by FINSEQ_2:10;
A29: k in Seg (len p) by A27, FINSEQ_1:def_3;
then A30: [i,k] in [:(Seg F2()),(Seg F3()):] by A10, A22, A25, ZFMISC_1:87;
 z = f . (i,k) by A25, A26, A28, A29;
hence  z in F1() by A30, FUNCT_2:5; ::_thesis: verum
end;
then reconsider p = p as FinSequence of F1() by FINSEQ_1:def_4;
take  p ; ::_thesis: ( x = p & len p = F3() )
thus  ( x = p & len p = F3() ) by A24, A25; ::_thesis: verum
end;
then reconsider M = M as Matrix of F1() by Th9;
 for p being FinSequence of F1() st p in rng M holds
len p = F3()
proof
let p be FinSequence of F1(); ::_thesis: ( p in rng M implies len p = F3() )
assume  p in rng M ; ::_thesis: len p = F3()
then consider i being Nat such that
A31: ( i in dom M & M . i = p ) by FINSEQ_2:10;
 S2[i,p] by A10, A11, A31;
hence  len p = F3() ; ::_thesis: verum
end;
then reconsider M = M as Matrix of F2(),F3(),F1() by A12, Def2;
take  M ; ::_thesis: for i, j being Nat st [i,j] in Indices M holds
P1[i,j,M * (i,j)]
let i, j be Nat; ::_thesis: ( [i,j] in Indices M implies P1[i,j,M * (i,j)] )
assume A32: [i,j] in Indices M ; ::_thesis: P1[i,j,M * (i,j)]
then  F2() <> 0 by A10, ZFMISC_1:87;
then A33: F2() > 0 by A7, XXREAL_0:1;
 j in Seg (width M) by A32, ZFMISC_1:87;
then A34: j in Seg F3() by A12, A33, Th20;
A35: ex p being FinSequence of F1() st
( p = M . i & M * (i,j) = p . j ) by A32, Def5;
A36: i in Seg F2() by A10, A32, ZFMISC_1:87;
then  ex q being FinSequence st
( M . i = q & len q = F3() & ( for j being Nat st j in Seg F3() holds
q . j = f . (i,j) ) ) by A11;
then  f . (i,j) = M * (i,j) by A35, A34;
hence  P1[i,j,M * (i,j)] by A6, A36, A34; ::_thesis: verum
end;

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 & width M = 0 & Indices M = {} )
proof
let m be Nat; ::_thesis: for D being non empty set
for M being Matrix of 0 ,m,D holds
( len M = 0 & width M = 0 & Indices M = {} )
let D be non empty set ; ::_thesis: for M being Matrix of 0 ,m,D holds
( len M = 0 & width M = 0 & Indices M = {} )
let M be Matrix of 0 ,m,D; ::_thesis: ( len M = 0 & width M = 0 & Indices M = {} )
 len M = 0 by Def2;
then  width M = 0 by Def3;
then  Seg (width M) = 0 ;
hence  ( len M = 0 & width M = 0 & Indices M = {} ) by Def2, ZFMISC_1:90; ::_thesis: verum
end;

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 & width M = m & Indices M = [:(Seg n),(Seg m):] )
proof
let n, m be Nat; ::_thesis: for D being non empty set st n > 0 holds
for M being Matrix of n,m,D holds
( len M = n & width M = m & Indices M = [:(Seg n),(Seg m):] )
let D be non empty set ; ::_thesis: ( n > 0 implies for M being Matrix of n,m,D holds
( len M = n & width M = m & Indices M = [:(Seg n),(Seg m):] ) )
assume A1: n > 0 ; ::_thesis: for M being Matrix of n,m,D holds
( len M = n & width M = m & Indices M = [:(Seg n),(Seg m):] )
let M be Matrix of n,m,D; ::_thesis: ( len M = n & width M = m & Indices M = [:(Seg n),(Seg m):] )
 ( Seg (len M) = dom M & len M = n ) by Def2, FINSEQ_1:def_3;
hence  ( len M = n & width M = m & Indices M = [:(Seg n),(Seg m):] ) by A1, Th20; ::_thesis: verum
end;

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 & width M = n & Indices M = [:(Seg n),(Seg n):] )
proof
let n be Nat; ::_thesis: for D being non empty set
for M being Matrix of n,D holds
( len M = n & width M = n & Indices M = [:(Seg n),(Seg n):] )
let D be non empty set ; ::_thesis: for M being Matrix of n,D holds
( len M = n & width M = n & Indices M = [:(Seg n),(Seg n):] )
let M be Matrix of n,D; ::_thesis: ( len M = n & width M = n & Indices M = [:(Seg n),(Seg n):] )
A1: len M = n by Def2;
A2: 0 <= n by NAT_1:2;
A3: now__::_thesis:_(_(_n_=_0_&_width_M_=_0_)_or_(_n_>_0_&_width_M_=_n_)_)
percases ( n = 0 or n > 0 ) by A2, XXREAL_0:1;
case n = 0 ; ::_thesis: width M = 0
hence  width M = 0 by A1, Def3; ::_thesis: verum
end;
case n > 0 ; ::_thesis: width M = n
hence  width M = n by A1, Th20; ::_thesis: verum
end;
end;
end;
 Seg (len M) = dom M by FINSEQ_1:def_3;
hence  ( len M = n & width M = n & Indices M = [:(Seg n),(Seg n):] ) by A3, Def2; ::_thesis: verum
end;

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 & Indices M = [:(Seg n),(Seg (width M)):] )
proof
let n, m be Nat; ::_thesis: for D being non empty set
for M being Matrix of n,m,D holds
( len M = n & Indices M = [:(Seg n),(Seg (width M)):] )
let D be non empty set ; ::_thesis: for M being Matrix of n,m,D holds
( len M = n & Indices M = [:(Seg n),(Seg (width M)):] )
let M be Matrix of n,m,D; ::_thesis: ( len M = n & Indices M = [:(Seg n),(Seg (width M)):] )
 len M = n by Def2;
hence  ( len M = n & Indices M = [:(Seg n),(Seg (width M)):] ) by FINSEQ_1:def_3; ::_thesis: verum
end;

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
proof
let n, m be Nat; ::_thesis: for D being non empty set
for M1, M2 being Matrix of n,m,D holds Indices M1 = Indices M2
let D be non empty set ; ::_thesis: for M1, M2 being Matrix of n,m,D holds Indices M1 = Indices M2
let M1, M2 be Matrix of n,m,D; ::_thesis: Indices M1 = Indices M2
A1: len M1 = n by Def2;
A2: len M2 = n by Def2;
A3: 0 <= n by NAT_1:2;
A4: now__::_thesis:_width_M1_=_width_M2
percases ( n = 0 or n > 0 ) by A3, XXREAL_0:1;
supposeA5: n = 0 ; ::_thesis: width M1 = width M2
then  width M1 = 0 by A1, Def3;
hence  width M1 = width M2 by A2, A5, Def3; ::_thesis: verum
end;
supposeA6: n > 0 ; ::_thesis: width M1 = width M2
then  width M1 = m by A1, Th20;
hence  width M1 = width M2 by A2, A6, Th20; ::_thesis: verum
end;
end;
end;
 dom M1 = Seg n by A1, FINSEQ_1:def_3;
hence  Indices M1 = Indices M2 by A2, A4, FINSEQ_1:def_3; ::_thesis: verum
end;

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
proof
let n, m be Nat; ::_thesis: 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
let D be non empty set ; ::_thesis: 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
let M1, M2 be Matrix of n,m,D; ::_thesis: ( ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) ) implies M1 = M2 )
A1: len M1 = n by Th25;
A2: len M2 = n by Th25;
A3: 0 <= n by NAT_1:2;
A4: now__::_thesis:_width_M1_=_width_M2
percases ( n = 0 or n > 0 ) by A3, XXREAL_0:1;
supposeA5: n = 0 ; ::_thesis: width M1 = width M2
then  width M1 = 0 by A1, Def3;
hence  width M1 = width M2 by A2, A5, Def3; ::_thesis: verum
end;
supposeA6: n > 0 ; ::_thesis: width M1 = width M2
then  width M1 = m by A1, Th20;
hence  width M1 = width M2 by A2, A6, Th20; ::_thesis: verum
end;
end;
end;
assume  for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) ; ::_thesis: M1 = M2
hence  M1 = M2 by A1, A2, A4, Th21; ::_thesis: verum
end;

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
proof
let n be Nat; ::_thesis: 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
let D be non empty set ; ::_thesis: for M1 being Matrix of n,D
for i, j being Nat st [i,j] in Indices M1 holds
[j,i] in Indices M1
let M1 be Matrix of n,D; ::_thesis: for i, j being Nat st [i,j] in Indices M1 holds
[j,i] in Indices M1
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies [j,i] in Indices M1 )
assume  [i,j] in Indices M1 ; ::_thesis: [j,i] in Indices M1
then  [i,j] in [:(Seg n),(Seg n):] by Th24;
then A1: ( j in Seg n & i in Seg n ) by ZFMISC_1:87;
 Indices M1 = [:(Seg n),(Seg n):] by Th24;
hence  [j,i] in Indices M1 by A1, ZFMISC_1:87; ::_thesis: verum
end;

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 & ( for i, j being Nat holds
( [i,j] in Indices it iff [j,i] in Indices M ) ) & ( 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 & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) )
proof
now__::_thesis:_ex_b1_being_Matrix_of_D_st_
(_len_b1_=_width_M_&_(_for_i,_j_being_Nat_holds_
(_[i,j]_in_Indices_b1_iff_[j,i]_in_Indices_M_)_)_&_(_for_i,_j_being_Nat_st_[j,i]_in_Indices_M_holds_
b1_*_(i,j)_=_M_*_(j,i)_)_)
percases ( width M > 0 or width M = 0 ) by NAT_1:3;
supposeA1: width M > 0 ; ::_thesis: ex b1 being Matrix of D st
( len b1 = width M & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) )
deffunc H1( Nat, Nat) ->  Element of D = M * ($2,$1);
consider M1 being Matrix of width M, len M,D such that
A2: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = H1(i,j) from MATRIX_1:sch_1();
reconsider M9 = M1 as Matrix of D ;
 Seg (len M) = dom M by FINSEQ_1:def_3;
then A3: Indices M1 = [:(Seg (width M)),(dom M):] by A1, Th23;
thus  ex b1 being Matrix of D st
( len b1 = width M & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) ) ::_thesis: verum
proof
take  M9 ; ::_thesis: ( len M9 = width M & ( for i, j being Nat holds
( [i,j] in Indices M9 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
M9 * (i,j) = M * (j,i) ) )
thus  len M9 = width M by A1, Th23; ::_thesis: ( ( for i, j being Nat holds
( [i,j] in Indices M9 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
M9 * (i,j) = M * (j,i) ) )
thus  for i, j being Nat holds
( [i,j] in Indices M9 iff [j,i] in Indices M ) by A3, ZFMISC_1:88; ::_thesis: for i, j being Nat st [j,i] in Indices M holds
M9 * (i,j) = M * (j,i)
let i, j be Nat; ::_thesis: ( [j,i] in Indices M implies M9 * (i,j) = M * (j,i) )
assume  [j,i] in Indices M ; ::_thesis: M9 * (i,j) = M * (j,i)
then  [i,j] in Indices M9 by A3, ZFMISC_1:88;
hence  M9 * (i,j) = M * (j,i) by A2; ::_thesis: verum
end;
end;
supposeA4: width M = 0 ; ::_thesis: ex b1 being Matrix of D st
( len b1 = width M & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) )
reconsider M1 = {} as Matrix of D by Th13;
thus  ex b1 being Matrix of D st
( len b1 = width M & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) ) ::_thesis: verum
proof
take  M1 ; ::_thesis: ( len M1 = width M & ( for i, j being Nat holds
( [i,j] in Indices M1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
M1 * (i,j) = M * (j,i) ) )
A5: Indices M1 = [:{},(Seg (width M1)):] ;
 Seg (width M) = {} by A4;
hence  ( len M1 = width M & ( for i, j being Nat holds
( [i,j] in Indices M1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
M1 * (i,j) = M * (j,i) ) ) by A4, A5, ZFMISC_1:90; ::_thesis: verum
end;
end;
end;
end;
hence  ex b1 being Matrix of D st
( len b1 = width M & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Matrix of D st len b1 = width M & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) & len b2 = width M & ( for i, j being Nat holds
( [i,j] in Indices b2 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b2 * (i,j) = M * (j,i) ) holds
b1 = b2
proof
let M1, M2 be Matrix of D; ::_thesis: ( len M1 = width M & ( for i, j being Nat holds
( [i,j] in Indices M1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
M1 * (i,j) = M * (j,i) ) & len M2 = width M & ( for i, j being Nat holds
( [i,j] in Indices M2 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
M2 * (i,j) = M * (j,i) ) implies M1 = M2 )
assume that
A6: len M1 = width M and
A7: for i, j being Nat holds
( [i,j] in Indices M1 iff [j,i] in Indices M ) and
A8: for i, j being Nat st [j,i] in Indices M holds
M1 * (i,j) = M * (j,i) and
A9: len M2 = width M and
A10: for i, j being Nat holds
( [i,j] in Indices M2 iff [j,i] in Indices M ) and
A11: for i, j being Nat st [j,i] in Indices M holds
M2 * (i,j) = M * (j,i) ; ::_thesis: M1 = M2
A12: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_M1_holds_
M1_*_(i,j)_=_M2_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume  [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then A13: [j,i] in Indices M by A7;
then  M1 * (i,j) = M * (j,i) by A8;
hence  M1 * (i,j) = M2 * (i,j) by A11, A13; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_set_holds_
(_(_[x,y]_in_[:(dom_M1),(Seg_(width_M1)):]_implies_[x,y]_in_[:(dom_M2),(Seg_(width_M2)):]_)_&_(_[x,y]_in_[:(dom_M2),(Seg_(width_M2)):]_implies_[x,y]_in_[:(dom_M1),(Seg_(width_M1)):]_)_)
let x, y be set ; ::_thesis: ( ( [x,y] in [:(dom M1),(Seg (width M1)):] implies [x,y] in [:(dom M2),(Seg (width M2)):] ) & ( [x,y] in [:(dom M2),(Seg (width M2)):] implies [x,y] in [:(dom M1),(Seg (width M1)):] ) )
thus  ( [x,y] in [:(dom M1),(Seg (width M1)):] implies [x,y] in [:(dom M2),(Seg (width M2)):] ) ::_thesis: ( [x,y] in [:(dom M2),(Seg (width M2)):] implies [x,y] in [:(dom M1),(Seg (width M1)):] )
proof
assume A14: [x,y] in [:(dom M1),(Seg (width M1)):] ; ::_thesis: [x,y] in [:(dom M2),(Seg (width M2)):]
then  x in dom M1 by ZFMISC_1:87;
then reconsider i = x as Element of NAT ;
 y in Seg (width M1) by A14, ZFMISC_1:87;
then reconsider j = y as Element of NAT ;
 [j,i] in Indices M by A7, A14;
hence  [x,y] in [:(dom M2),(Seg (width M2)):] by A10; ::_thesis: verum
end;
thus  ( [x,y] in [:(dom M2),(Seg (width M2)):] implies [x,y] in [:(dom M1),(Seg (width M1)):] ) ::_thesis: verum
proof
assume A15: [x,y] in [:(dom M2),(Seg (width M2)):] ; ::_thesis: [x,y] in [:(dom M1),(Seg (width M1)):]
then  x in dom M2 by ZFMISC_1:87;
then reconsider i = x as Element of NAT ;
 y in Seg (width M2) by A15, ZFMISC_1:87;
then reconsider j = y as Element of NAT ;
 [j,i] in Indices M by A10, A15;
hence  [x,y] in [:(dom M1),(Seg (width M1)):] by A7; ::_thesis: verum
end;
end;
then A16: [:(dom M1),(Seg (width M1)):] = [:(dom M2),(Seg (width M2)):] by ZFMISC_1:89;
A17: now__::_thesis:_(_len_M1_<>_0_implies_(_len_M1_=_len_M2_&_width_M1_=_width_M2_)_)
assume A18: len M1 <> 0 ; ::_thesis: ( len M1 = len M2 & width M1 = width M2 )
then  Seg (len M2) <> {} by A6, A9;
then A19: dom M2 <> {} by FINSEQ_1:def_3;
now__::_thesis:_width_M1_=_width_M2
percases ( Seg (width M1) <> {} or Seg (width M1) = {} ) ;
supposeA20: Seg (width M1) <> {} ; ::_thesis: width M1 = width M2
 Seg (len M1) <> {} by A18;
then  dom M1 <> {} by FINSEQ_1:def_3;
then  Seg (width M1) = Seg (width M2) by A16, A20, ZFMISC_1:110;
hence  width M1 = width M2 by FINSEQ_1:6; ::_thesis: verum
end;
supposeA21: Seg (width M1) = {} ; ::_thesis: width M1 = width M2
then  [:(dom M2),(Seg (width M2)):] = {} by A16, ZFMISC_1:90;
then  Seg (width M2) = {} by A19, ZFMISC_1:90;
hence  width M1 = width M2 by A21, FINSEQ_1:6; ::_thesis: verum
end;
end;
end;
hence  ( len M1 = len M2 & width M1 = width M2 ) by A6, A9; ::_thesis: verum
end;
 ( len M1 = 0 implies ( len M2 = 0 & width M1 = 0 & width M2 = 0 ) ) by A6, A9, Def3;
hence  M1 = M2 by A17, A12, Th21; ::_thesis: verum
end;
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 & ( for i, j being Nat holds
( [i,j] in Indices b3 iff [j,i] in Indices M ) ) & ( 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 & width (M @) = len M )
proof
let D be non empty set ; ::_thesis: for M being Matrix of D st width M > 0 holds
( len (M @) = width M & width (M @) = len M )
let M be Matrix of D; ::_thesis: ( width M > 0 implies ( len (M @) = width M & width (M @) = len M ) )
assume A1: width M > 0 ; ::_thesis: ( len (M @) = width M & width (M @) = len M )
thus  len (M @) = width M by Def6; ::_thesis: width (M @) = len M
A2: len M >= 0 by NAT_1:2;
percases ( len M = 0 or len M > 0 ) by A2, XXREAL_0:1;
suppose len M = 0 ; ::_thesis: width (M @) = len M
hence  width (M @) = len M by A1, Def3; ::_thesis: verum
end;
supposeA3: len M > 0 ; ::_thesis: width (M @) = len M
 for i, j being set holds
( [i,j] in [:(dom (M @)),(Seg (width (M @))):] iff [i,j] in [:(Seg (width M)),(dom M):] )
proof
let i, j be set ; ::_thesis: ( [i,j] in [:(dom (M @)),(Seg (width (M @))):] iff [i,j] in [:(Seg (width M)),(dom M):] )
thus  ( [i,j] in [:(dom (M @)),(Seg (width (M @))):] implies [i,j] in [:(Seg (width M)),(dom M):] ) ::_thesis: ( [i,j] in [:(Seg (width M)),(dom M):] implies [i,j] in [:(dom (M @)),(Seg (width (M @))):] )
proof
assume A4: [i,j] in [:(dom (M @)),(Seg (width (M @))):] ; ::_thesis: [i,j] in [:(Seg (width M)),(dom M):]
then  ( i in dom (M @) & j in Seg (width (M @)) ) by ZFMISC_1:87;
then reconsider i = i, j = j as Element of NAT ;
 [i,j] in Indices (M @) by A4;
then  [j,i] in Indices M by Def6;
hence  [i,j] in [:(Seg (width M)),(dom M):] by ZFMISC_1:88; ::_thesis: verum
end;
assume A5: [i,j] in [:(Seg (width M)),(dom M):] ; ::_thesis: [i,j] in [:(dom (M @)),(Seg (width (M @))):]
then  ( i in Seg (width M) & j in dom M ) by ZFMISC_1:87;
then reconsider i = i, j = j as Element of NAT ;
 [j,i] in Indices M by A5, ZFMISC_1:88;
then  [i,j] in Indices (M @) by Def6;
hence  [i,j] in [:(dom (M @)),(Seg (width (M @))):] ; ::_thesis: verum
end;
then  ( dom M = Seg (len M) & [:(Seg (width M)),(dom M):] = [:(dom (M @)),(Seg (width (M @))):] ) by FINSEQ_1:def_3, ZFMISC_1:89;
then  dom M = Seg (width (M @)) by A1, A3, ZFMISC_1:110;
hence  width (M @) = len M by FINSEQ_1:def_3; ::_thesis: verum
end;
end;
end;

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
proof
let n be Element of NAT ; ::_thesis: for K being non empty set
for A being Matrix of n,K holds A @ is Matrix of n,K
let K be non empty set ; ::_thesis: for A being Matrix of n,K holds A @ is Matrix of n,K
let A be Matrix of n,K; ::_thesis: A @ is Matrix of n,K
A1: len A = n by Def2;
A2: for p being FinSequence of K st p in rng (A @) holds
len p = n
proof
let p be FinSequence of K; ::_thesis: ( p in rng (A @) implies len p = n )
consider n2 being Nat such that
A3: for x being set st x in rng (A @) holds
ex s being FinSequence st
( s = x & len s = n2 ) by Def1;
A4: for p2 being FinSequence of K st p2 in rng (A @) holds
len p2 = n2
proof
let p2 be FinSequence of K; ::_thesis: ( p2 in rng (A @) implies len p2 = n2 )
assume  p2 in rng (A @) ; ::_thesis: len p2 = n2
then  ex s being FinSequence st
( s = p2 & len s = n2 ) by A3;
hence  len p2 = n2 ; ::_thesis: verum
end;
assume A5: p in rng (A @) ; ::_thesis: len p = n
then A6: ex s being FinSequence st
( s = p & len s = n2 ) by A3;
now__::_thesis:_(_(_n_>_0_&_len_p_=_n_)_or_(_n_<=_0_&_len_p_=_n_)_)
percases ( n > 0 or n <= 0 ) ;
caseA7: n > 0 ; ::_thesis: len p = n
then A8: width A = n by A1, Th20;
then A9: width (A @) = len A by A7, Lm1;
A10: len (A @) = width A by A7, A8, Lm1;
then  A @ is Matrix of n,n2,K by A4, A8, Def2;
hence  len p = n by A1, A6, A7, A8, A10, A9, Th20; ::_thesis: verum
end;
caseA11: n <= 0 ; ::_thesis: len p = n
A12: ( len (A @) = width A & ex x0 being set st
( x0 in dom (A @) & p = (A @) . x0 ) ) by A5, Def6, FUNCT_1:def_3;
 width A = 0 by A1, A11, Def3;
then  Seg (width A) = {} ;
hence  len p = n by A12, FINSEQ_1:def_3; ::_thesis: verum
end;
end;
end;
hence  len p = n ; ::_thesis: verum
end;
A13: len (A @) = width A by Def6;
now__::_thesis:_(_(_n_>_0_&_len_(A_@)_=_n_)_or_(_n_=_0_&_len_(A_@)_=_n_)_)
A14: n >= 0 by NAT_1:2;
percases ( n > 0 or n = 0 ) by A14, XXREAL_0:1;
case n > 0 ; ::_thesis: len (A @) = n
hence  len (A @) = n by A13, A1, Th20; ::_thesis: verum
end;
case n = 0 ; ::_thesis: len (A @) = n
hence  len (A @) = n by A13, A1, Def3; ::_thesis: verum
end;
end;
end;
hence  A @ is Matrix of n,K by A2, Def2; ::_thesis: verum
end;

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
proof
 n in NAT by ORDINAL1:def_12;
hence  M @ is Matrix of n,D by Lm2; ::_thesis: verum
end;
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 & ( 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 & ( for j being Nat st j in Seg (width M) holds
b1 . j = M * (i,j) ) )
proof
deffunc H1( Nat) ->  Element of D = M * (i,$1);
consider f being FinSequence of D such that
A1: len f = width M and
A2: for j being Nat st j in dom f holds
f . j = H1(j) from FINSEQ_2:sch_1();
take  f ; ::_thesis: ( len f = width M & ( for j being Nat st j in Seg (width M) holds
f . j = M * (i,j) ) )
thus  len f = width M by A1; ::_thesis: for j being Nat st j in Seg (width M) holds
f . j = M * (i,j)
let j be Nat; ::_thesis: ( j in Seg (width M) implies f . j = M * (i,j) )
 dom f = Seg (width M) by A1, FINSEQ_1:def_3;
hence  ( j in Seg (width M) implies f . j = M * (i,j) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of D st len b1 = width M & ( for j being Nat st j in Seg (width M) holds
b1 . j = M * (i,j) ) & len b2 = width M & ( for j being Nat st j in Seg (width M) holds
b2 . j = M * (i,j) ) holds
b1 = b2
proof
let p1, p2 be FinSequence of D; ::_thesis: ( len p1 = width M & ( for j being Nat st j in Seg (width M) holds
p1 . j = M * (i,j) ) & len p2 = width M & ( for j being Nat st j in Seg (width M) holds
p2 . j = M * (i,j) ) implies p1 = p2 )
assume that
A3: len p1 = width M and
A4: for j being Nat st j in Seg (width M) holds
p1 . j = M * (i,j) and
A5: len p2 = width M and
A6: for j being Nat st j in Seg (width M) holds
p2 . j = M * (i,j) ; ::_thesis: p1 = p2
A7: dom p1 = Seg (width M) by A3, FINSEQ_1:def_3;
 for j being Nat st j in dom p1 holds
p1 . j = p2 . j
proof
let j be Nat; ::_thesis: ( j in dom p1 implies p1 . j = p2 . j )
assume A8: j in dom p1 ; ::_thesis: p1 . j = p2 . j
then  p1 . j = M * (i,j) by A4, A7;
hence  p1 . j = p2 . j by A6, A7, A8; ::_thesis: verum
end;
hence  p1 = p2 by A3, A5, FINSEQ_2:9; ::_thesis: verum
end;
func Col (M,i) ->  FinSequence of D means :Def8: :: MATRIX_1:def 8
( len it = len M & ( 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 & ( for j being Nat st j in dom M holds
b1 . j = M * (j,i) ) )
proof
deffunc H1( Nat) ->  Element of D = M * ($1,i);
consider z being FinSequence of D such that
A9: len z = len M and
A10: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
take  z ; ::_thesis: ( len z = len M & ( for j being Nat st j in dom M holds
z . j = M * (j,i) ) )
thus  len z = len M by A9; ::_thesis: for j being Nat st j in dom M holds
z . j = M * (j,i)
let j be Nat; ::_thesis: ( j in dom M implies z . j = M * (j,i) )
A11: Seg (len M) = dom M by FINSEQ_1:def_3;
 dom z = Seg (len M) by A9, FINSEQ_1:def_3;
hence  ( j in dom M implies z . j = M * (j,i) ) by A10, A11; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of D st len b1 = len M & ( for j being Nat st j in dom M holds
b1 . j = M * (j,i) ) & len b2 = len M & ( for j being Nat st j in dom M holds
b2 . j = M * (j,i) ) holds
b1 = b2
proof
let p1, p2 be FinSequence of D; ::_thesis: ( len p1 = len M & ( for j being Nat st j in dom M holds
p1 . j = M * (j,i) ) & len p2 = len M & ( for j being Nat st j in dom M holds
p2 . j = M * (j,i) ) implies p1 = p2 )
assume that
A12: len p1 = len M and
A13: for j being Nat st j in dom M holds
p1 . j = M * (j,i) and
A14: len p2 = len M and
A15: for j being Nat st j in dom M holds
p2 . j = M * (j,i) ; ::_thesis: p1 = p2
A16: dom p1 = Seg (len M) by A12, FINSEQ_1:def_3;
 for j being Nat st j in dom p1 holds
p1 . j = p2 . j
proof
let j be Nat; ::_thesis: ( j in dom p1 implies p1 . j = p2 . j )
assume  j in dom p1 ; ::_thesis: p1 . j = p2 . j
then A17: j in dom M by A16, FINSEQ_1:def_3;
then  p1 . j = M * (j,i) by A13;
hence  p1 . j = p2 . j by A15, A17; ::_thesis: verum
end;
hence  p1 = p2 by A12, A14, FINSEQ_2:9; ::_thesis: verum
end;
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 & ( 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 & ( 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
proof
 ( len (Line (M,i)) = width M & Line (M,i) is Element of D * ) by Def7, FINSEQ_1:def_11;
then  Line (M,i) in  {  p where p is Element of D * : len p = width M  }  ;
hence  Line (M,i) is Element of (width M) -tuples_on D ; ::_thesis: verum
end;
:: 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
proof
 ( len (Col (M,i)) = len M & Col (M,i) is Element of D * ) by Def8, FINSEQ_1:def_11;
then  Col (M,i) in  {  p where p is Element of D * : len p = len M  }  ;
hence  Col (M,i) is Element of (len M) -tuples_on D ; ::_thesis: verum
end;
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 ) & ( for i, j being Nat st [i,j] in Indices it & 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 ) & ( for i, j being Nat st [i,j] in Indices b1 & i <> j holds
b1 * (i,j) = 0. K ) )
proof
defpred S1[ set , set , set ] means ( ( $1 = $2 implies $3 = 1. K ) & ( $1 <> $2 implies $3 = 0. K ) );
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
A1: for i, j being Nat st [i,j] in [:(Seg n1),(Seg n1):] holds
ex x being Element of K st S1[i,j,x]
proof
let i, j be Nat; ::_thesis: ( [i,j] in [:(Seg n1),(Seg n1):] implies ex x being Element of K st S1[i,j,x] )
assume  [i,j] in [:(Seg n1),(Seg n1):] ; ::_thesis: ex x being Element of K st S1[i,j,x]
 ( i = j implies S1[i,j, 1. K] ) ;
hence  ex x being Element of K st S1[i,j,x] ; ::_thesis: verum
end;
consider M being Matrix of n1,K such that
A2: for i, j being Nat st [i,j] in Indices M holds
S1[i,j,M * (i,j)] from MATRIX_1:sch_2(A1);
reconsider M = M as Matrix of n,K ;
take  M ; ::_thesis: ( ( for i being Nat st [i,i] in Indices M holds
M * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices M & i <> j holds
M * (i,j) = 0. K ) )
thus  ( ( for i being Nat st [i,i] in Indices M holds
M * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices M & i <> j holds
M * (i,j) = 0. K ) ) by A2; ::_thesis: verum
end;
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 ) & ( for i, j being Nat st [i,j] in Indices b1 & i <> j holds
b1 * (i,j) = 0. K ) & ( for i being Nat st [i,i] in Indices b2 holds
b2 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices b2 & i <> j holds
b2 * (i,j) = 0. K ) holds
b1 = b2
proof
let M1, M2 be Matrix of n,K; ::_thesis: ( ( for i being Nat st [i,i] in Indices M1 holds
M1 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices M1 & i <> j holds
M1 * (i,j) = 0. K ) & ( for i being Nat st [i,i] in Indices M2 holds
M2 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices M2 & i <> j holds
M2 * (i,j) = 0. K ) implies M1 = M2 )
assume that
A3: for i being Nat st [i,i] in Indices M1 holds
M1 * (i,i) = 1. K and
A4: for i, j being Nat st [i,j] in Indices M1 & i <> j holds
M1 * (i,j) = 0. K and
A5: for i being Nat st [i,i] in Indices M2 holds
M2 * (i,i) = 1. K and
A6: for i, j being Nat st [i,j] in Indices M2 & i <> j holds
M2 * (i,j) = 0. K ; ::_thesis: M1 = M2
A7: Indices M1 = Indices M2 by Th26;
A8: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_M1_holds_
M1_*_(i,j)_=_M2_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A9: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
A10: now__::_thesis:_(_i_<>_j_implies_M1_*_(i,j)_=_M2_*_(i,j)_)
assume A11: i <> j ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then  M1 * (i,j) = 0. K by A4, A9;
hence  M1 * (i,j) = M2 * (i,j) by A7, A6, A9, A11; ::_thesis: verum
end;
now__::_thesis:_(_i_=_j_implies_M1_*_(i,j)_=_M2_*_(i,j)_)
assume A12: i = j ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then  M1 * (i,j) = 1. K by A3, A9;
hence  M1 * (i,j) = M2 * (i,j) by A7, A5, A9, A12; ::_thesis: verum
end;
hence  M1 * (i,j) = M2 * (i,j) by A10; ::_thesis: verum
end;
A13: ( len M2 = n & width M2 = n ) by Th24;
 ( len M1 = n & width M1 = n ) by Th24;
hence  M1 = M2 by A8, A13, Th21; ::_thesis: verum
end;
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))
proof
deffunc H1( Nat, Nat) ->  Element of the carrier of K = - (A * ($1,$2));
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
consider M being Matrix of n1,K such that
A14: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = H1(i,j) from MATRIX_1:sch_1();
 Indices A = [:(Seg n),(Seg n):] by Th24;
then A15: Indices A = Indices M by Th24;
reconsider M = M as Matrix of n,K ;
take  M ; ::_thesis: for i, j being Nat st [i,j] in Indices A holds
M * (i,j) = - (A * (i,j))
thus  for i, j being Nat st [i,j] in Indices A holds
M * (i,j) = - (A * (i,j)) by A14, A15; ::_thesis: verum
end;
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)) ) & ( for i, j being Nat st [i,j] in Indices A holds
b2 * (i,j) = - (A * (i,j)) ) holds
b1 = b2
proof
let M1, M2 be Matrix of n,K; ::_thesis: ( ( for i, j being Nat st [i,j] in Indices A holds
M1 * (i,j) = - (A * (i,j)) ) & ( for i, j being Nat st [i,j] in Indices A holds
M2 * (i,j) = - (A * (i,j)) ) implies M1 = M2 )
assume that
A16: for i, j being Nat st [i,j] in Indices A holds
M1 * (i,j) = - (A * (i,j)) and
A17: for i, j being Nat st [i,j] in Indices A holds
M2 * (i,j) = - (A * (i,j)) ; ::_thesis: M1 = M2
A18: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_A_holds_
M1_*_(i,j)_=_M2_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies M1 * (i,j) = M2 * (i,j) )
assume A19: [i,j] in Indices A ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then  M1 * (i,j) = - (A * (i,j)) by A16;
hence  M1 * (i,j) = M2 * (i,j) by A17, A19; ::_thesis: verum
end;
 Indices M1 = [:(Seg n),(Seg n):] by Th24;
then  Indices A = Indices M1 by Th24;
hence  M1 = M2 by A18, Th27; ::_thesis: verum
end;
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))
proof
deffunc H1( Nat, Nat) ->  Element of the carrier of K = (A * ($1,$2)) + (B * ($1,$2));
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
consider M being Matrix of n1,K such that
A20: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = H1(i,j) from MATRIX_1:sch_1();
 Indices A = [:(Seg n),(Seg n):] by Th24;
then A21: Indices A = Indices M by Th24;
reconsider M = M as Matrix of n,K ;
take  M ; ::_thesis: for i, j being Nat st [i,j] in Indices A holds
M * (i,j) = (A * (i,j)) + (B * (i,j))
thus  for i, j being Nat st [i,j] in Indices A holds
M * (i,j) = (A * (i,j)) + (B * (i,j)) by A20, A21; ::_thesis: verum
end;
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)) ) & ( 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
let M1, M2 be Matrix of n,K; ::_thesis: ( ( for i, j being Nat st [i,j] in Indices A holds
M1 * (i,j) = (A * (i,j)) + (B * (i,j)) ) & ( for i, j being Nat st [i,j] in Indices A holds
M2 * (i,j) = (A * (i,j)) + (B * (i,j)) ) implies M1 = M2 )
assume that
A22: for i, j being Nat st [i,j] in Indices A holds
M1 * (i,j) = (A * (i,j)) + (B * (i,j)) and
A23: for i, j being Nat st [i,j] in Indices A holds
M2 * (i,j) = (A * (i,j)) + (B * (i,j)) ; ::_thesis: M1 = M2
A24: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_A_holds_
M1_*_(i,j)_=_M2_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies M1 * (i,j) = M2 * (i,j) )
assume A25: [i,j] in Indices A ; ::_thesis: M1 * (i,j) = M2 * (i,j)
then  M1 * (i,j) = (A * (i,j)) + (B * (i,j)) by A22;
hence  M1 * (i,j) = M2 * (i,j) by A23, A25; ::_thesis: verum
end;
 Indices M1 = [:(Seg n),(Seg n):] by Th24;
then  Indices A = Indices M1 by Th24;
hence  M1 = M2 by A24, Th27; ::_thesis: verum
end;
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 ) & ( for i, j being Nat st [i,j] in Indices b3 & 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
proof
let i, j, n be Nat; ::_thesis: for K being non empty doubleLoopStr st [i,j] in Indices (0. (K,n)) holds
(0. (K,n)) * (i,j) = 0. K
let K be non empty doubleLoopStr ; ::_thesis: ( [i,j] in Indices (0. (K,n)) implies (0. (K,n)) * (i,j) = 0. K )
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
set M = 0. (K,n);
assume A1: [i,j] in Indices (0. (K,n)) ; ::_thesis: (0. (K,n)) * (i,j) = 0. K
then A2: [i,j] in [:(Seg n),(Seg n):] by Th24;
then  j in Seg n by ZFMISC_1:87;
then A3: (n1 |-> (0. K)) . j = 0. K by FUNCOP_1:7;
 i in Seg n by A2, ZFMISC_1:87;
then  (0. (K,n)) . i = n1 |-> (0. K) by FUNCOP_1:7;
hence  (0. (K,n)) * (i,j) = 0. K by A1, A3, Def5; ::_thesis: verum
end;

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 )
proof
let x be set ; ::_thesis: 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 )
let n be Nat; ::_thesis: for K being non empty doubleLoopStr holds
( x is Element of n -Matrices_over K iff x is Matrix of n,K )
let K be non empty doubleLoopStr ; ::_thesis: ( x is Element of n -Matrices_over K iff x is Matrix of n,K )
thus  ( x is Element of n -Matrices_over K implies x is Matrix of n,K ) ::_thesis: ( x is Matrix of n,K implies x is Element of n -Matrices_over K )
proof
assume  x is Element of n -Matrices_over K ; ::_thesis: x is Matrix of n,K
then reconsider x = x as Element of n -tuples_on (n -tuples_on the carrier of K) ;
A1: len x = n by CARD_1:def_7;
 ex m being Nat st
for y being set st y in rng x holds
ex q being FinSequence of K st
( y = q & len q = m )
proof
take  n ; ::_thesis: for y being set st y in rng x holds
ex q being FinSequence of K st
( y = q & len q = n )
let y be set ; ::_thesis: ( y in rng x implies ex q being FinSequence of K st
( y = q & len q = n ) )
A2: rng x c= n -tuples_on the carrier of K by FINSEQ_1:def_4;
assume  y in rng x ; ::_thesis: ex q being FinSequence of K st
( y = q & len q = n )
then reconsider q = y as Element of n -tuples_on the carrier of K by A2;
reconsider q = q as FinSequence of K ;
take  q ; ::_thesis: ( y = q & len q = n )
thus  ( y = q & len q = n ) by CARD_1:def_7; ::_thesis: verum
end;
then reconsider x = x as Matrix of the carrier of K by Th9;
 for q being FinSequence of K st q in rng x holds
len q = n
proof
let q be FinSequence of K; ::_thesis: ( q in rng x implies len q = n )
A3: rng x c= n -tuples_on the carrier of K by FINSEQ_1:def_4;
assume  q in rng x ; ::_thesis: len q = n
then reconsider q = q as Element of n -tuples_on the carrier of K by A3;
 len q = n by CARD_1:def_7;
hence  len q = n ; ::_thesis: verum
end;
hence  x is Matrix of n,K by A1, Def2; ::_thesis: verum
end;
assume  x is Matrix of n,K ; ::_thesis: x is Element of n -Matrices_over K
then reconsider x = x as Matrix of n,K ;
A4: len x = n by Def2;
then reconsider x = x as Element of n -tuples_on ( the carrier of K *) by FINSEQ_2:92;
 rng x c= n -tuples_on the carrier of K
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng x or y in n -tuples_on the carrier of K )
assume A5: y in rng x ; ::_thesis: y in n -tuples_on the carrier of K
 rng x c= the carrier of K * by FINSEQ_1:def_4;
then reconsider p = y as FinSequence of K by A5, FINSEQ_1:def_11;
 len p = n by A5, Def2;
then  p is Element of n -tuples_on the carrier of K by FINSEQ_2:92;
hence  y in n -tuples_on the carrier of K ; ::_thesis: verum
end;
then  x is FinSequence of n -tuples_on the carrier of K by FINSEQ_1:def_4;
hence  x is Element of n -Matrices_over K by A4, FINSEQ_2:92; ::_thesis: verum
end;

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 & 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 & 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
proof
take  1. (K,n) ; ::_thesis: 1. (K,n) is diagonal
let i be Nat; :: according to MATRIX_1:def_14 ::_thesis: for j being Nat st [i,j] in Indices (1. (K,n)) & (1. (K,n)) * (i,j) <> 0. K holds
i = j
let j be Nat; ::_thesis: ( [i,j] in Indices (1. (K,n)) & (1. (K,n)) * (i,j) <> 0. K implies i = j )
thus  ( [i,j] in Indices (1. (K,n)) & (1. (K,n)) * (i,j) <> 0. K implies i = j ) by Def11; ::_thesis: verum
end;
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
proof
let n be Nat; ::_thesis: 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
let F be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for A, B being Matrix of n,F holds A + B = B + A
let A, B be Matrix of n,F; ::_thesis: A + B = B + A
A1: Indices A = Indices (A + B) by Th26;
A2: Indices A = Indices B by Th26;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_(A_+_B)_holds_
(A_+_B)_*_(i,j)_=_(B_+_A)_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices (A + B) implies (A + B) * (i,j) = (B + A) * (i,j) )
assume A3: [i,j] in Indices (A + B) ; ::_thesis: (A + B) * (i,j) = (B + A) * (i,j)
hence (A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) by A1, Def13
.= (B + A) * (i,j) by A2, A1, A3, Def13 ;
::_thesis: verum
end;
hence  A + B = B + A by Th27; ::_thesis: verum
end;

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)
proof
let n be Nat; ::_thesis: 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)
let F be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for A, B, C being Matrix of n,F holds (A + B) + C = A + (B + C)
let A, B, C be Matrix of n,F; ::_thesis: (A + B) + C = A + (B + C)
A1: Indices A = Indices ((A + B) + C) by Th26;
A2: Indices A = Indices (A + B) by Th26;
A3: Indices A = Indices B by Th26;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((A_+_B)_+_C)_holds_
((A_+_B)_+_C)_*_(i,j)_=_(A_+_(B_+_C))_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((A + B) + C) implies ((A + B) + C) * (i,j) = (A + (B + C)) * (i,j) )
assume A4: [i,j] in Indices ((A + B) + C) ; ::_thesis: ((A + B) + C) * (i,j) = (A + (B + C)) * (i,j)
hence ((A + B) + C) * (i,j) = ((A + B) * (i,j)) + (C * (i,j)) by A1, A2, Def13
.= ((A * (i,j)) + (B * (i,j))) + (C * (i,j)) by A1, A4, Def13
.= (A * (i,j)) + ((B * (i,j)) + (C * (i,j))) by RLVECT_1:def_3
.= (A * (i,j)) + ((B + C) * (i,j)) by A3, A1, A4, Def13
.= (A + (B + C)) * (i,j) by A1, A4, Def13 ;
::_thesis: verum
end;
hence  (A + B) + C = A + (B + C) by Th27; ::_thesis: verum
end;

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
proof
let n be Nat; ::_thesis: 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
let F be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for A being Matrix of n,F holds A + (0. (F,n)) = A
let A be Matrix of n,F; ::_thesis: A + (0. (F,n)) = A
A1: Indices A = Indices (A + (0. (F,n))) by Th26;
A2: Indices A = Indices (0. (F,n)) by Th26;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_(A_+_(0._(F,n)))_holds_
(A_+_(0._(F,n)))_*_(i,j)_=_A_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices (A + (0. (F,n))) implies (A + (0. (F,n))) * (i,j) = A * (i,j) )
assume A3: [i,j] in Indices (A + (0. (F,n))) ; ::_thesis: (A + (0. (F,n))) * (i,j) = A * (i,j)
hence (A + (0. (F,n))) * (i,j) = (A * (i,j)) + ((0. (F,n)) * (i,j)) by A1, Def13
.= (A * (i,j)) + (0. F) by A1, A2, A3, Th29
.= A * (i,j) by RLVECT_1:4 ;
::_thesis: verum
end;
hence  A + (0. (F,n)) = A by Th27; ::_thesis: verum
end;

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)
proof
let n be Nat; ::_thesis: 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)
let F be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for A being Matrix of n,F holds A + (- A) = 0. (F,n)
let A be Matrix of n,F; ::_thesis: A + (- A) = 0. (F,n)
A1: Indices A = Indices (A + (- A)) by Th26;
A2: Indices A = Indices (0. (F,n)) by Th26;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_(A_+_(-_A))_holds_
(A_+_(-_A))_*_(i,j)_=_(0._(F,n))_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices (A + (- A)) implies (A + (- A)) * (i,j) = (0. (F,n)) * (i,j) )
assume A3: [i,j] in Indices (A + (- A)) ; ::_thesis: (A + (- A)) * (i,j) = (0. (F,n)) * (i,j)
hence (A + (- A)) * (i,j) = (A * (i,j)) + ((- A) * (i,j)) by A1, Def13
.= (A * (i,j)) + (- (A * (i,j))) by A1, A3, Def12
.= 0. F by RLVECT_1:def_10
.= (0. (F,n)) * (i,j) by A2, A1, A3, Th29 ;
::_thesis: verum
end;
hence  A + (- A) = 0. (F,n) by Th27; ::_thesis: verum
end;

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 & ( for A, B being Matrix of n,F holds the addF of it . (A,B) = A + B ) & 0. it = 0. (F,n) );
existence
 ex b1 being strict AbGroup st
( the carrier of b1 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b1 . (A,B) = A + B ) & 0. b1 = 0. (F,n) )
proof
reconsider A0 = 0. (F,n) as Element of n -Matrices_over F ;
defpred S1[ Element of n -Matrices_over F, Element of n -Matrices_over F, Element of n -Matrices_over F] means  ex A, B being Matrix of n,F st
( $1 = A & $2 = B & $3 = A + B );
A1: for a, b being Element of n -Matrices_over F ex c being Element of n -Matrices_over F st S1[a,b,c]
proof
let a, b be Element of n -Matrices_over F; ::_thesis: ex c being Element of n -Matrices_over F st S1[a,b,c]
reconsider B = b as Matrix of n,F by Th30;
reconsider A = a as Matrix of n,F by Th30;
reconsider c = A + B as Element of n -Matrices_over F by Th30;
take  c ; ::_thesis: S1[a,b,c]
thus  S1[a,b,c] ; ::_thesis: verum
end;
consider h being BinOp of (n -Matrices_over F) such that
A2: for a, b being Element of n -Matrices_over F holds S1[a,b,h . (a,b)] from BINOP_1:sch_3(A1);
set G = addLoopStr(# (n -Matrices_over F),h,A0 #);
A3: for A, B being Matrix of n,F holds h . (A,B) = A + B
proof
let A, B be Matrix of n,F; ::_thesis: h . (A,B) = A + B
 ( A is Element of n -Matrices_over F & B is Element of n -Matrices_over F ) by Th30;
then  ex A9, B9 being Matrix of n,F st
( A = A9 & B = B9 & h . (A,B) = A9 + B9 ) by A2;
hence  h . (A,B) = A + B ; ::_thesis: verum
end;
A4: for a being Element of n -Matrices_over F ex b being Element of n -Matrices_over F ex A being Matrix of n,F st
( a = A & b = - A )
proof
let a be Element of n -Matrices_over F; ::_thesis: ex b being Element of n -Matrices_over F ex A being Matrix of n,F st
( a = A & b = - A )
reconsider A = a as Matrix of n,F by Th30;
reconsider b = - A as Element of n -Matrices_over F by Th30;
take  b ; ::_thesis: ex A being Matrix of n,F st
( a = A & b = - A )
thus  ex A being Matrix of n,F st
( a = A & b = - A ) ; ::_thesis: verum
end;
 ( addLoopStr(# (n -Matrices_over F),h,A0 #) is Abelian & addLoopStr(# (n -Matrices_over F),h,A0 #) is add-associative & addLoopStr(# (n -Matrices_over F),h,A0 #) is right_zeroed & addLoopStr(# (n -Matrices_over F),h,A0 #) is right_complementable )
proof
thus  addLoopStr(# (n -Matrices_over F),h,A0 #) is Abelian ::_thesis: ( addLoopStr(# (n -Matrices_over F),h,A0 #) is add-associative & addLoopStr(# (n -Matrices_over F),h,A0 #) is right_zeroed & addLoopStr(# (n -Matrices_over F),h,A0 #) is right_complementable )
proof
let a, b be Element of addLoopStr(# (n -Matrices_over F),h,A0 #); :: according to RLVECT_1:def_2 ::_thesis: a + b = b + a
reconsider A = a, B = b as Matrix of n,F by Th30;
thus a + b = A + B by A3
.= B + A by Th31
.= b + a by A3 ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_3 ::_thesis: ( addLoopStr(# (n -Matrices_over F),h,A0 #) is right_zeroed & addLoopStr(# (n -Matrices_over F),h,A0 #) is right_complementable )
let a, b, c be Element of addLoopStr(# (n -Matrices_over F),h,A0 #); ::_thesis: (a + b) + c = a + (b + c)
reconsider A = a, B = b, C = c as Matrix of n,F by Th30;
thus (a + b) + c = h . ((A + B),C) by A3
.= (A + B) + C by A3
.= A + (B + C) by Th32
.= h . (A,(B + C)) by A3
.= a + (b + c) by A3 ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_4 ::_thesis: addLoopStr(# (n -Matrices_over F),h,A0 #) is right_complementable
let a be Element of addLoopStr(# (n -Matrices_over F),h,A0 #); ::_thesis: a + (0. addLoopStr(# (n -Matrices_over F),h,A0 #)) = a
reconsider A = a as Matrix of n,F by Th30;
thus a + (0. addLoopStr(# (n -Matrices_over F),h,A0 #)) = A + (0. (F,n)) by A3
.= a by Th33 ; ::_thesis: verum
end;
let a be Element of addLoopStr(# (n -Matrices_over F),h,A0 #); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable
consider b being Element of n -Matrices_over F such that
A5: ex A being Matrix of n,F st
( a = A & b = - A ) by A4;
consider A being Matrix of n,F such that
A6: a = A and
A7: b = - A by A5;
reconsider b = - A as Element of addLoopStr(# (n -Matrices_over F),h,A0 #) by A7;
take  b ; :: according to ALGSTR_0:def_11 ::_thesis: a + b = 0. addLoopStr(# (n -Matrices_over F),h,A0 #)
thus a + b = A + (- A) by A3, A6
.= 0. addLoopStr(# (n -Matrices_over F),h,A0 #) by Th34 ; ::_thesis: verum
end;
then reconsider G = addLoopStr(# (n -Matrices_over F),h,A0 #) as strict AbGroup ;
take  G ; ::_thesis: ( the carrier of G = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of G . (A,B) = A + B ) & 0. G = 0. (F,n) )
thus  ( the carrier of G = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of G . (A,B) = A + B ) & 0. G = 0. (F,n) ) by A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict AbGroup st the carrier of b1 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b1 . (A,B) = A + B ) & 0. b1 = 0. (F,n) & the carrier of b2 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b2 . (A,B) = A + B ) & 0. b2 = 0. (F,n) holds
b1 = b2
proof
thus  for G1, G2 being strict AbGroup st the carrier of G1 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of G1 . (A,B) = A + B ) & 0. G1 = 0. (F,n) & the carrier of G2 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of G2 . (A,B) = A + B ) & 0. G2 = 0. (F,n) holds
G1 = G2 ::_thesis: verum
proof
let G1, G2 be strict AbGroup; ::_thesis: ( the carrier of G1 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of G1 . (A,B) = A + B ) & 0. G1 = 0. (F,n) & the carrier of G2 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of G2 . (A,B) = A + B ) & 0. G2 = 0. (F,n) implies G1 = G2 )
assume that
A8: the carrier of G1 = n -Matrices_over F and
A9: for A, B being Matrix of n,F holds the addF of G1 . (A,B) = A + B and
A10: ( 0. G1 = 0. (F,n) & the carrier of G2 = n -Matrices_over F ) and
A11: for A, B being Matrix of n,F holds the addF of G2 . (A,B) = A + B and
A12: 0. G2 = 0. (F,n) ; ::_thesis: G1 = G2
now__::_thesis:_for_a,_b_being_Element_of_G1_holds_the_addF_of_G1_._(a,b)_=_the_addF_of_G2_._(a,b)
let a, b be Element of G1; ::_thesis: the addF of G1 . (a,b) = the addF of G2 . (a,b)
reconsider A = a, B = b as Matrix of n,F by A8, Th30;
thus  the addF of G1 . (a,b) = A + B by A9
.= the addF of G2 . (a,b) by A11 ; ::_thesis: verum
end;
hence  G1 = G2 by A8, A10, A12, BINOP_1:2; ::_thesis: verum
end;
end;
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 & ( for A, B being Matrix of n,F holds the addF of b3 . (A,B) = A + B ) & 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
proof
let n, m be Nat; ::_thesis: 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
let K be non empty doubleLoopStr ; ::_thesis: for M1 being Matrix of 0 ,n,K
for M2 being Matrix of 0 ,m,K holds M1 = M2
let M1 be Matrix of 0 ,n,K; ::_thesis: for M2 being Matrix of 0 ,m,K holds M1 = M2
let M2 be Matrix of 0 ,m,K; ::_thesis: M1 = M2
 ( len M1 = 0 & len M2 = 0 ) by Def2;
hence  M1 = M2 by CARD_2:64; ::_thesis: verum
end;

begin

theorem Th36: :: MATRIX_1:36
for D being set
for i, j being Nat
for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
[i,j] in Indices M
proof
let D be set ; ::_thesis: for i, j being Nat
for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
[i,j] in Indices M
let i, j be Nat; ::_thesis: for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
[i,j] in Indices M
let M be Matrix of D; ::_thesis: ( 1 <= i & i <= len M & 1 <= j & j <= width M implies [i,j] in Indices M )
assume  ( 1 <= i & i <= len M & 1 <= j & j <= width M ) ; ::_thesis: [i,j] in Indices M
then  ( i in dom M & j in Seg (width M) ) by FINSEQ_1:1, FINSEQ_3:25;
hence  [i,j] in Indices M by ZFMISC_1:87; ::_thesis: verum
end;

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 & i <= n & 1 <= j & j <= m holds
[i,j] in Indices M
proof
let n, m, i, j be Nat; ::_thesis: for D being non empty set
for M being Matrix of n,m,D st 1 <= i & i <= n & 1 <= j & j <= m holds
[i,j] in Indices M
let D be non empty set ; ::_thesis: for M being Matrix of n,m,D st 1 <= i & i <= n & 1 <= j & j <= m holds
[i,j] in Indices M
let M be Matrix of n,m,D; ::_thesis: ( 1 <= i & i <= n & 1 <= j & j <= m implies [i,j] in Indices M )
assume that
A1: ( 1 <= i & i <= n ) and
A2: ( 1 <= j & j <= m ) ; ::_thesis: [i,j] in Indices M
A3: len M = n by Def2;
percases ( n = 0 or n > 0 ) by NAT_1:3;
suppose n = 0 ; ::_thesis: [i,j] in Indices M
hence  [i,j] in Indices M by A1, XXREAL_0:2; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: [i,j] in Indices M
then  m = width M by Th23;
hence  [i,j] in Indices M by A1, A2, A3, Th36; ::_thesis: verum
end;
end;
end;

theorem Th38: :: MATRIX_1:38
for M being tabular FinSequence
for i, j being Nat st [i,j] in Indices M holds
( 1 <= i & i <= len M & 1 <= j & j <= width M )
proof
let M be tabular FinSequence; ::_thesis: for i, j being Nat st [i,j] in Indices M holds
( 1 <= i & i <= len M & 1 <= j & j <= width M )
let i, j be Nat; ::_thesis: ( [i,j] in Indices M implies ( 1 <= i & i <= len M & 1 <= j & j <= width M ) )
assume  [i,j] in Indices M ; ::_thesis: ( 1 <= i & i <= len M & 1 <= j & j <= width M )
then  ( i in dom M & j in Seg (width M) ) by ZFMISC_1:87;
hence  ( 1 <= i & i <= len M & 1 <= j & j <= width M ) by FINSEQ_1:1, FINSEQ_3:25; ::_thesis: verum
end;

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 & i <= n & 1 <= j & j <= m )
proof
let n, m, i, j be Nat; ::_thesis: for D being non empty set
for M being Matrix of n,m,D st [i,j] in Indices M holds
( 1 <= i & i <= n & 1 <= j & j <= m )
let D be non empty set ; ::_thesis: for M being Matrix of n,m,D st [i,j] in Indices M holds
( 1 <= i & i <= n & 1 <= j & j <= m )
let M be Matrix of n,m,D; ::_thesis: ( [i,j] in Indices M implies ( 1 <= i & i <= n & 1 <= j & j <= m ) )
assume A1: [i,j] in Indices M ; ::_thesis: ( 1 <= i & i <= n & 1 <= j & j <= m )
A2: len M = n by Def2;
percases ( n = 0 or n > 0 ) by NAT_1:3;
supposeA3: n = 0 ; ::_thesis: ( 1 <= i & i <= n & 1 <= j & j <= m )
A4: i in dom M by A1, ZFMISC_1:87;
then A5: 1 <= i by FINSEQ_3:25;
 i <= 0 by A2, A3, A4, FINSEQ_3:25;
hence  ( 1 <= i & i <= n & 1 <= j & j <= m ) by A5, XXREAL_0:2; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: ( 1 <= i & i <= n & 1 <= j & j <= m )
then  m = width M by Th23;
hence  ( 1 <= i & i <= n & 1 <= j & j <= m ) by A1, A2, Th38; ::_thesis: verum
end;
end;
end;

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
proof
let i be Nat; ::_thesis: for D being non empty set
for M being FinSequence of D * holds M . i is FinSequence of D
let D be non empty set ; ::_thesis: for M being FinSequence of D * holds M . i is FinSequence of D
let M be FinSequence of D * ; ::_thesis: M . i is FinSequence of D
percases ( not i in dom M or i in dom M ) ;
suppose not i in dom M ; ::_thesis: M . i is FinSequence of D
then  M . i = <*> D by FUNCT_1:def_2;
hence  M . i is FinSequence of D ; ::_thesis: verum
end;
supposeA1: i in dom M ; ::_thesis: M . i is FinSequence of D
A2: rng M c= D * by FINSEQ_1:def_4;
 M . i in rng M by A1, FUNCT_1:def_3;
hence  M . i is FinSequence of D by A2, FINSEQ_1:def_11; ::_thesis: verum
end;
end;
end;

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  }
proof
let D be non empty set ; ::_thesis: for M being FinSequence of D * holds Values M = union  {  (rng f) where f is Element of D * : f in rng M  }
let M be FinSequence of D * ; ::_thesis: Values M = union  {  (rng f) where f is Element of D * : f in rng M  }
set R =  {  (rng f) where f is Element of D * : f in rng M  }  ;
A1: Union (rngs M) = union (rng (rngs M)) by CARD_3:def_4;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_Values_M_implies_y_in_union__{__(rng_f)_where_f_is_Element_of_D_*_:_f_in_rng_M__}__)_&_(_y_in_union__{__(rng_f)_where_f_is_Element_of_D_*_:_f_in_rng_M__}__implies_y_in_Values_M_)_)
let y be set ; ::_thesis: ( ( y in Values M implies y in union  {  (rng f) where f is Element of D * : f in rng M  }  ) & ( y in union  {  (rng f) where f is Element of D * : f in rng M  }  implies y in Values M ) )
hereby  ::_thesis: ( y in union  {  (rng f) where f is Element of D * : f in rng M  }  implies y in Values M )
assume  y in Values M ; ::_thesis: y in union  {  (rng f) where f is Element of D * : f in rng M  }
then consider Y being set  such that
A2: y in Y and
A3: Y in rng (rngs M) by A1, TARSKI:def_4;
consider i being set  such that
A4: i in dom (rngs M) and
A5: (rngs M) . i = Y by A3, FUNCT_1:def_3;
A6: i in dom M by A4, FUNCT_6:60;
then reconsider i = i as Element of NAT ;
reconsider f = M . i as FinSequence of D by Th40;
A7: Y = rng f by A5, A6, FUNCT_6:22;
A8: f in D * by FINSEQ_1:def_11;
 f in rng M by A6, FUNCT_1:def_3;
then  rng f in  {  (rng f) where f is Element of D * : f in rng M  }  by A8;
hence  y in union  {  (rng f) where f is Element of D * : f in rng M  }  by A2, A7, TARSKI:def_4; ::_thesis: verum
end;
assume  y in union  {  (rng f) where f is Element of D * : f in rng M  }  ; ::_thesis: y in Values M
then consider Y being set  such that
A9: y in Y and
A10: Y in  {  (rng f) where f is Element of D * : f in rng M  }  by TARSKI:def_4;
consider f being Element of D *  such that
A11: Y = rng f and
A12: f in rng M by A10;
consider i being Nat such that
A13: ( i in dom M & M . i = f ) by A12, FINSEQ_2:10;
 ( i in dom (rngs M) & (rngs M) . i = rng f ) by A13, FUNCT_6:22;
then  rng f in rng (rngs M) by FUNCT_1:def_3;
hence  y in Values M by A1, A9, A11, TARSKI:def_4; ::_thesis: verum
end;
hence  Values M = union  {  (rng f) where f is Element of D * : f in rng M  }  by TARSKI:1; ::_thesis: verum
end;

registration
let D be non empty set ;
let M be FinSequence of D * ;
cluster Values M ->  finite ;
coherence
 Values M is finite
proof
deffunc H1( Function) ->  set = rng D;
set A =  {  H1(f) where f is Element of D * : f in rng M  }  ;
A1: now__::_thesis:_for_X_being_set_st_X_in__{__H1(f)_where_f_is_Element_of_D_*_:_f_in_rng_M__}__holds_
X_is_finite
let X be set ; ::_thesis: ( X in  {  H1(f) where f is Element of D * : f in rng M  }  implies X is finite )
assume  X in  {  H1(f) where f is Element of D * : f in rng M  }  ; ::_thesis: X is finite
then  ex f being Element of D * st
( X = rng f & f in rng M ) ;
hence  X is finite ; ::_thesis: verum
end;
A2: rng M is finite ;
  {  H1(f) where f is Element of D * : f in rng M  }  is finite from FRAENKEL:sch_21(A2);
then  union  {  H1(f) where f is Element of D * : f in rng M  }  is finite by A1, FINSET_1:7;
hence  Values M is finite by Th41; ::_thesis: verum
end;
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 & M . i = f holds
len f = width M
proof
let i be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D
for M being Matrix of D st i in dom M & M . i = f holds
len f = width M
let D be non empty set ; ::_thesis: for f being FinSequence of D
for M being Matrix of D st i in dom M & M . i = f holds
len f = width M
let f be FinSequence of D; ::_thesis: for M being Matrix of D st i in dom M & M . i = f holds
len f = width M
let M be Matrix of D; ::_thesis: ( i in dom M & M . i = f implies len f = width M )
assume that
A1: i in dom M and
A2: M . i = f ; ::_thesis: len f = width M
 not M is empty by A1;
then  len M > 0 by NAT_1:3;
then consider p being FinSequence such that
A3: p in rng M and
A4: len p = width M by Def3;
consider n being Nat such that
A5: for x being set st x in rng M holds
ex s being FinSequence st
( s = x & len s = n ) by Def1;
 M . i in rng M by A1, FUNCT_1:def_3;
then A6: ex s being FinSequence st
( s = M . i & len s = n ) by A5;
 ex s being FinSequence st
( s = p & len s = n ) by A3, A5;
hence  len f = width M by A2, A4, A6; ::_thesis: verum
end;

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 & M . i = f & j in dom f holds
[i,j] in Indices M
proof
let i, j be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D
for M being Matrix of D st i in dom M & M . i = f & j in dom f holds
[i,j] in Indices M
let D be non empty set ; ::_thesis: for f being FinSequence of D
for M being Matrix of D st i in dom M & M . i = f & j in dom f holds
[i,j] in Indices M
let f be FinSequence of D; ::_thesis: for M being Matrix of D st i in dom M & M . i = f & j in dom f holds
[i,j] in Indices M
let M be Matrix of D; ::_thesis: ( i in dom M & M . i = f & j in dom f implies [i,j] in Indices M )
assume that
A1: i in dom M and
A2: ( M . i = f & j in dom f ) ; ::_thesis: [i,j] in Indices M
 not M is empty by A1;
then  len M > 0 by NAT_1:3;
then consider p being FinSequence such that
A3: p in rng M and
A4: len p = width M by Def3;
consider n being Nat such that
A5: for x being set st x in rng M holds
ex s being FinSequence st
( s = x & len s = n ) by Def1;
 M . i in rng M by A1, FUNCT_1:def_3;
then A6: ex s being FinSequence st
( s = M . i & len s = n ) by A5;
 ex s being FinSequence st
( s = p & len s = n ) by A3, A5;
then  ( Indices M = [:(dom M),(Seg (width M)):] & j in Seg (width M) ) by A2, A4, A6, FINSEQ_1:def_3;
hence  [i,j] in Indices M by A1, ZFMISC_1:87; ::_thesis: verum
end;

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 & M . i = f holds
( len f = width M & j in dom f )
proof
let i, j be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D
for M being Matrix of D st [i,j] in Indices M & M . i = f holds
( len f = width M & j in dom f )
let D be non empty set ; ::_thesis: for f being FinSequence of D
for M being Matrix of D st [i,j] in Indices M & M . i = f holds
( len f = width M & j in dom f )
let f be FinSequence of D; ::_thesis: for M being Matrix of D st [i,j] in Indices M & M . i = f holds
( len f = width M & j in dom f )
let M be Matrix of D; ::_thesis: ( [i,j] in Indices M & M . i = f implies ( len f = width M & j in dom f ) )
assume A1: [i,j] in Indices M ; ::_thesis: ( not M . i = f or ( len f = width M & j in dom f ) )
A2: j in Seg (width M) by A1, ZFMISC_1:87;
 not M is empty by A1, ZFMISC_1:87;
then  len M > 0 by NAT_1:3;
then consider p being FinSequence such that
A3: p in rng M and
A4: len p = width M by Def3;
consider n being Nat such that
A5: for x being set st x in rng M holds
ex s being FinSequence st
( s = x & len s = n ) by Def1;
 i in dom M by A1, ZFMISC_1:87;
then  M . i in rng M by FUNCT_1:def_3;
then A6: ex s being FinSequence st
( s = M . i & len s = n ) by A5;
 ex s being FinSequence st
( s = p & len s = n ) by A3, A5;
hence  ( not M . i = f or ( len f = width M & j in dom f ) ) by A2, A4, A6, FINSEQ_1:def_3; ::_thesis: verum
end;

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  }
proof
let D be non empty set ; ::_thesis: for M being Matrix of D holds Values M =  {  (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M  }
let M be Matrix of D; ::_thesis: Values M =  {  (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M  }
set V =  {  (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M  }  ;
set R =  {  (rng f) where f is Element of D * : f in rng M  }  ;
A1: Values M = union  {  (rng f) where f is Element of D * : f in rng M  }  by Th41;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_Values_M_implies_y_in__{__(M_*_(i,j))_where_i,_j_is_Element_of_NAT_:_[i,j]_in_Indices_M__}__)_&_(_y_in__{__(M_*_(i,j))_where_i,_j_is_Element_of_NAT_:_[i,j]_in_Indices_M__}__implies_y_in_Values_M_)_)
let y be set ; ::_thesis: ( ( y in Values M implies y in  {  (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M  }  ) & ( y in  {  (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M  }  implies y in Values M ) )
hereby  ::_thesis: ( y in  {  (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M  }  implies y in Values M )
assume  y in Values M ; ::_thesis: y in  {  (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M  }
then consider Y being set  such that
A2: y in Y and
A3: Y in  {  (rng f) where f is Element of D * : f in rng M  }  by A1, TARSKI:def_4;
consider f being Element of D *  such that
A4: Y = rng f and
A5: f in rng M by A3;
consider j being Nat such that
A6: j in dom f and
A7: f . j = y by A2, A4, FINSEQ_2:10;
consider i being Nat such that
A8: i in dom M and
A9: M . i = f by A5, FINSEQ_2:10;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def_12;
A10: [i,j] in Indices M by A8, A9, A6, Th43;
then  ex p being FinSequence of D st
( p = M . i & M * (i,j) = p . j ) by Def5;
hence  y in  {  (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M  }  by A9, A7, A10; ::_thesis: verum
end;
assume  y in  {  (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M  }  ; ::_thesis: y in Values M
then consider i, j being Element of NAT  such that
A11: y = M * (i,j) and
A12: [i,j] in Indices M ;
consider f being FinSequence of D such that
A13: f = M . i and
A14: M * (i,j) = f . j by A12, Def5;
 j in dom f by A12, A13, Th44;
then A15: f . j in rng f by FUNCT_1:def_3;
 i in dom M by A12, ZFMISC_1:87;
then A16: M . i in rng M by FUNCT_1:def_3;
 f in D * by FINSEQ_1:def_11;
then  rng f in  {  (rng f) where f is Element of D * : f in rng M  }  by A13, A16;
hence  y in Values M by A1, A11, A14, A15, TARSKI:def_4; ::_thesis: verum
end;
hence  Values M =  {  (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M  }  by TARSKI:1; ::_thesis: verum
end;

theorem :: MATRIX_1:46
for D being non empty set
for M being Matrix of D holds card (Values M) <= (len M) * (width M)
proof
let D be non empty set ; ::_thesis: for M being Matrix of D holds card (Values M) <= (len M) * (width M)
let M be Matrix of D; ::_thesis: card (Values M) <= (len M) * (width M)
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_(rngs_M)_holds_
card_((rngs_M)_._x)_c=_card_(width_M)
let x be set ; ::_thesis: ( x in dom (rngs M) implies card ((rngs M) . x) c= card (width M) )
assume  x in dom (rngs M) ; ::_thesis: card ((rngs M) . x) c= card (width M)
then A2: x in dom M by FUNCT_6:60;
then reconsider i = x as Element of NAT ;
reconsider f = M . i as FinSequence of D by Th40;
 card (rng f) c= card (dom f) by CARD_2:61;
then  card (rng f) c= card (Seg (len f)) by FINSEQ_1:def_3;
then  card (rng f) c= card (len f) by FINSEQ_1:55;
then  card (rng f) c= card (width M) by A2, Th42;
hence  card ((rngs M) . x) c= card (width M) by A2, FUNCT_6:22; ::_thesis: verum
end;
card (dom (rngs M)) = card (dom M) by FUNCT_6:60
.= card (len M) by CARD_1:62 ;
then  card (Union (rngs M)) c= (card (len M)) *` (card (width M)) by A1, CARD_2:86;
then  card (Values M) c= card ((len M) * (width M)) by CARD_2:39;
then  card (Values M) <= card ((len M) * (width M)) by NAT_1:39;
hence  card (Values M) <= (len M) * (width M) by CARD_1:def_2; ::_thesis: verum
end;


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 & i <= len M & 1 <= j & j <= width M holds
M * (i,j) in Values M
proof
let D be non empty set ; ::_thesis: for i, j being Element of NAT
for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
M * (i,j) in Values M
let i, j be Element of NAT ; ::_thesis: for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
M * (i,j) in Values M
let M be Matrix of D; ::_thesis: ( 1 <= i & i <= len M & 1 <= j & j <= width M implies M * (i,j) in Values M )
assume  ( 1 <= i & i <= len M & 1 <= j & j <= width M ) ; ::_thesis: M * (i,j) in Values M
then A1: [i,j] in Indices M by Th36;
 Values M =  {  (M * (i1,j1)) where i1, j1 is Element of NAT : [i1,j1] in Indices M  }  by Th45;
hence  M * (i,j) in Values M by A1; ::_thesis: verum
end;