:: MATRIX_2 semantic presentation

begin


definition
let n, m be Nat;
let a be set ;
func(n,m) --> a ->  tabular FinSequence equals :: MATRIX_2:def 1
n |-> (m |-> a);
coherence
 n |-> (m |-> a) is tabular FinSequence by MATRIX_1:2;
end;

:: deftheorem  defines --> MATRIX_2:def_1_:_
 for n, m being Nat
for a being set holds (n,m) --> a = n |-> (m |-> a);

definition
let D be non empty set ;
let n, m be Nat;
let d be Element of D;
:: original: -->
redefine func(n,m) --> d ->  Matrix of n,m,D;
coherence
 (n,m) --> d is Matrix of n,m,D by MATRIX_1:10;
end;

theorem Th1: :: MATRIX_2:1
for i, j, n, m being Nat
for D being non empty set
for a being Element of D st [i,j] in Indices ((n,m) --> a) holds
((n,m) --> a) * (i,j) = a
proof
let i, j, n, m be Nat; ::_thesis: for D being non empty set
for a being Element of D st [i,j] in Indices ((n,m) --> a) holds
((n,m) --> a) * (i,j) = a
let D be non empty set ; ::_thesis: for a being Element of D st [i,j] in Indices ((n,m) --> a) holds
((n,m) --> a) * (i,j) = a
let a be Element of D; ::_thesis: ( [i,j] in Indices ((n,m) --> a) implies ((n,m) --> a) * (i,j) = a )
reconsider m1 = m as Element of NAT by ORDINAL1:def_12;
set M = (n,m) --> a;
assume A1: [i,j] in Indices ((n,m) --> a) ; ::_thesis: ((n,m) --> a) * (i,j) = a
then  i in dom ((n,m) --> a) by ZFMISC_1:87;
then  i in Seg (len ((n,m) --> a)) by FINSEQ_1:def_3;
then A2: i in Seg n by MATRIX_1:def_2;
then A3: n > 0 ;
 j in Seg (width ((n,m) --> a)) by A1, ZFMISC_1:87;
then  j in Seg m by A3, MATRIX_1:23;
then A4: (m1 |-> a) . j = a by FUNCOP_1:7;
 ((n,m) --> a) . i = m1 |-> a by A2, FUNCOP_1:7;
hence  ((n,m) --> a) * (i,j) = a by A1, A4, MATRIX_1:def_5; ::_thesis: verum
end;

theorem :: MATRIX_2:2
for n being Nat
for K being Field
for a9, b9 being Element of K holds ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9)
proof
let n be Nat; ::_thesis: for K being Field
for a9, b9 being Element of K holds ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9)
let K be Field; ::_thesis: for a9, b9 being Element of K holds ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9)
let a9, b9 be Element of K; ::_thesis: ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9)
A1: Indices ((n,n) --> a9) = Indices ((n,n) --> (a9 + b9)) by MATRIX_1:26;
A2: Indices ((n,n) --> a9) = Indices ((n,n) --> b9) by MATRIX_1:26;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((n,n)_-->_(a9_+_b9))_holds_
(((n,n)_-->_a9)_*_(i,j))_+_(((n,n)_-->_b9)_*_(i,j))_=_((n,n)_-->_(a9_+_b9))_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((n,n) --> (a9 + b9)) implies (((n,n) --> a9) * (i,j)) + (((n,n) --> b9) * (i,j)) = ((n,n) --> (a9 + b9)) * (i,j) )
assume A3: [i,j] in Indices ((n,n) --> (a9 + b9)) ; ::_thesis: (((n,n) --> a9) * (i,j)) + (((n,n) --> b9) * (i,j)) = ((n,n) --> (a9 + b9)) * (i,j)
then  ((n,n) --> a9) * (i,j) = a9 by A1, Th1;
then  (((n,n) --> a9) * (i,j)) + (((n,n) --> b9) * (i,j)) = a9 + b9 by A2, A1, A3, Th1;
hence  (((n,n) --> a9) * (i,j)) + (((n,n) --> b9) * (i,j)) = ((n,n) --> (a9 + b9)) * (i,j) by A3, Th1; ::_thesis: verum
end;
hence  ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9) by A1, MATRIX_1:def_13; ::_thesis: verum
end;

definition
let a, b, c, d be set ;
func(a,b) ][ (c,d) ->  tabular FinSequence equals :: MATRIX_2:def 2
<*<*a,b*>,<*c,d*>*>;
correctness
coherence
<*<*a,b*>,<*c,d*>*> is tabular FinSequence;
proof
 ( len <*a,b*> = 2 & len <*c,d*> = 2 ) by FINSEQ_1:44;
hence  <*<*a,b*>,<*c,d*>*> is tabular FinSequence by MATRIX_1:4; ::_thesis: verum
end;
end;

:: deftheorem  defines ][ MATRIX_2:def_2_:_
 for a, b, c, d being set holds (a,b) ][ (c,d) = <*<*a,b*>,<*c,d*>*>;

theorem Th3: :: MATRIX_2:3
for x1, x2, y1, y2 being set holds
( len ((x1,x2) ][ (y1,y2)) = 2 & width ((x1,x2) ][ (y1,y2)) = 2 & Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] )
proof
let x1, x2, y1, y2 be set ; ::_thesis: ( len ((x1,x2) ][ (y1,y2)) = 2 & width ((x1,x2) ][ (y1,y2)) = 2 & Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] )
set M = (x1,x2) ][ (y1,y2);
thus A1: len ((x1,x2) ][ (y1,y2)) = 2 by FINSEQ_1:44; ::_thesis: ( width ((x1,x2) ][ (y1,y2)) = 2 & Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] )
 rng ((x1,x2) ][ (y1,y2)) = {<*x1,x2*>,<*y1,y2*>} by FINSEQ_2:127;
then A2: <*x1,x2*> in rng ((x1,x2) ][ (y1,y2)) by TARSKI:def_2;
 len <*x1,x2*> = 2 by FINSEQ_1:44;
hence  width ((x1,x2) ][ (y1,y2)) = 2 by A1, A2, MATRIX_1:def_3; ::_thesis: Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):]
hence  Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] by A1, FINSEQ_1:def_3; ::_thesis: verum
end;

theorem Th4: :: MATRIX_2:4
for x1, x2, y1, y2 being set holds
( [1,1] in Indices ((x1,x2) ][ (y1,y2)) & [1,2] in Indices ((x1,x2) ][ (y1,y2)) & [2,1] in Indices ((x1,x2) ][ (y1,y2)) & [2,2] in Indices ((x1,x2) ][ (y1,y2)) )
proof
let x1, x2, y1, y2 be set ; ::_thesis: ( [1,1] in Indices ((x1,x2) ][ (y1,y2)) & [1,2] in Indices ((x1,x2) ][ (y1,y2)) & [2,1] in Indices ((x1,x2) ][ (y1,y2)) & [2,2] in Indices ((x1,x2) ][ (y1,y2)) )
A1: 2 in Seg 2 by FINSEQ_1:2, TARSKI:def_2;
 ( Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] & 1 in Seg 2 ) by Th3, FINSEQ_1:2, TARSKI:def_2;
hence  ( [1,1] in Indices ((x1,x2) ][ (y1,y2)) & [1,2] in Indices ((x1,x2) ][ (y1,y2)) & [2,1] in Indices ((x1,x2) ][ (y1,y2)) & [2,2] in Indices ((x1,x2) ][ (y1,y2)) ) by A1, ZFMISC_1:87; ::_thesis: verum
end;

definition
let D be non empty set ;
let a be Element of D;
:: original: <*
redefine func<*a*> ->  Element of 1 -tuples_on D;
coherence
 <*a*> is Element of 1 -tuples_on D by FINSEQ_2:98;
end;

definition
let D be non empty set ;
let n be Nat;
let p be Element of n -tuples_on D;
:: original: <*
redefine func<*p*> ->  Matrix of 1,n,D;
coherence
 <*p*> is Matrix of 1,n,D
proof
 len p = n by CARD_1:def_7;
hence  <*p*> is Matrix of 1,n,D by MATRIX_1:11; ::_thesis: verum
end;
end;

theorem :: MATRIX_2:5
for D being non empty set
for a being Element of D holds
( [1,1] in Indices <*<*a*>*> & <*<*a*>*> * (1,1) = a )
proof
let D be non empty set ; ::_thesis: for a being Element of D holds
( [1,1] in Indices <*<*a*>*> & <*<*a*>*> * (1,1) = a )
let a be Element of D; ::_thesis: ( [1,1] in Indices <*<*a*>*> & <*<*a*>*> * (1,1) = a )
set M = <*<*a*>*>;
 ( Indices <*<*a*>*> = [:(Seg 1),(Seg 1):] & 1 in Seg 1 ) by FINSEQ_1:2, MATRIX_1:24, TARSKI:def_1;
hence A1: [1,1] in Indices <*<*a*>*> by ZFMISC_1:87; ::_thesis: <*<*a*>*> * (1,1) = a
 ( <*<*a*>*> . 1 = <*a*> & <*a*> . 1 = a ) by FINSEQ_1:40;
hence  <*<*a*>*> * (1,1) = a by A1, MATRIX_1:def_5; ::_thesis: verum
end;

definition
let D be non empty set ;
let a, b, c, d be Element of D;
:: original: ][
redefine func(a,b) ][ (c,d) ->  Matrix of 2,D;
coherence
 (a,b) ][ (c,d) is Matrix of 2,D by MATRIX_1:19;
end;

theorem :: MATRIX_2:6
for D being non empty set
for a, b, c, d being Element of D holds
( ((a,b) ][ (c,d)) * (1,1) = a & ((a,b) ][ (c,d)) * (1,2) = b & ((a,b) ][ (c,d)) * (2,1) = c & ((a,b) ][ (c,d)) * (2,2) = d )
proof
let D be non empty set ; ::_thesis: for a, b, c, d being Element of D holds
( ((a,b) ][ (c,d)) * (1,1) = a & ((a,b) ][ (c,d)) * (1,2) = b & ((a,b) ][ (c,d)) * (2,1) = c & ((a,b) ][ (c,d)) * (2,2) = d )
let a, b, c, d be Element of D; ::_thesis: ( ((a,b) ][ (c,d)) * (1,1) = a & ((a,b) ][ (c,d)) * (1,2) = b & ((a,b) ][ (c,d)) * (2,1) = c & ((a,b) ][ (c,d)) * (2,2) = d )
set M = (a,b) ][ (c,d);
A1: ( ((a,b) ][ (c,d)) . 1 = <*a,b*> & ((a,b) ][ (c,d)) . 2 = <*c,d*> ) by FINSEQ_1:44;
A2: ( <*a,b*> . 1 = a & <*a,b*> . 2 = b ) by FINSEQ_1:44;
A3: ( [2,1] in Indices ((a,b) ][ (c,d)) & [2,2] in Indices ((a,b) ][ (c,d)) ) by Th4;
A4: ( <*c,d*> . 1 = c & <*c,d*> . 2 = d ) by FINSEQ_1:44;
 ( [1,1] in Indices ((a,b) ][ (c,d)) & [1,2] in Indices ((a,b) ][ (c,d)) ) by Th4;
hence  ( ((a,b) ][ (c,d)) * (1,1) = a & ((a,b) ][ (c,d)) * (1,2) = b & ((a,b) ][ (c,d)) * (2,1) = c & ((a,b) ][ (c,d)) * (2,2) = d ) by A1, A2, A4, A3, MATRIX_1:def_5; ::_thesis: verum
end;

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
attrM is upper_triangular  means :Def3: :: MATRIX_2:def 3
 for i, j being Nat st [i,j] in Indices M & i > j holds
M * (i,j) = 0. K;
attrM is lower_triangular  means :: MATRIX_2:def 4
 for i, j being Nat st [i,j] in Indices M & i < j holds
M * (i,j) = 0. K;
end;

:: deftheorem Def3 defines upper_triangular MATRIX_2:def_3_:_
 for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is upper_triangular iff for i, j being Nat st [i,j] in Indices M & i > j holds
M * (i,j) = 0. K );

:: deftheorem  defines lower_triangular MATRIX_2:def_4_:_
 for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is lower_triangular iff for i, j being Nat st [i,j] in Indices M & i < j holds
M * (i,j) = 0. K );

registration
let n be Nat;
let K be Field;
cluster diagonal  ->  upper_triangular lower_triangular for Matrix of n,n, the carrier of K;
coherence
 for b1 being Diagonal of n,K holds
( b1 is upper_triangular & b1 is lower_triangular )
proof
let M be Diagonal of n,K; ::_thesis: ( M is upper_triangular & M is lower_triangular )
 for i, j being Nat st [i,j] in Indices M & i > j holds
M * (i,j) = 0. K by MATRIX_1:def_14;
hence  M is upper_triangular by Def3; ::_thesis: M is lower_triangular
thus  for i, j being Nat st [i,j] in Indices M & i < j holds
M * (i,j) = 0. K by MATRIX_1:def_14; :: according to MATRIX_2:def_4 ::_thesis: verum
end;
end;

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular upper_triangular lower_triangular for Matrix of n,n, the carrier of K;
existence
 ex b1 being Matrix of n,K st
( b1 is lower_triangular & b1 is upper_triangular )
proof
set M = the Diagonal of n,K;
take  the Diagonal of n,K ; ::_thesis: ( the Diagonal of n,K is lower_triangular & the Diagonal of n,K is upper_triangular )
thus  ( the Diagonal of n,K is lower_triangular & the Diagonal of n,K is upper_triangular ) ; ::_thesis: verum
end;
end;

definition
let n be Nat;
let K be Field;
mode Upper_Triangular_Matrix of n,K is upper_triangular Matrix of n,K;
mode Lower_Triangular_Matrix of n,K is lower_triangular Matrix of n,K;
end;

theorem :: MATRIX_2:7
for n being Nat
for D being non empty set
for M being Matrix of D st len M = n holds
M is Matrix of n, width M,D
proof
let n be Nat; ::_thesis: for D being non empty set
for M being Matrix of D st len M = n holds
M is Matrix of n, width M,D
let D be non empty set ; ::_thesis: for M being Matrix of D st len M = n holds
M is Matrix of n, width M,D
let M be Matrix of D; ::_thesis: ( len M = n implies M is Matrix of n, width M,D )
assume that
A1: len M = n and
A2: M is not Matrix of n, width M,D ; ::_thesis: contradiction
set m = width M;
percases ( len M <> n or ex p being FinSequence of D st
( p in rng M & not len p = width M ) ) by A2, MATRIX_1:def_2;
suppose len M <> n ; ::_thesis: contradiction
hence  contradiction by A1; ::_thesis: verum
end;
supposeA3: ex p being FinSequence of D st
( p in rng M & not len p = width M ) ; ::_thesis: contradiction
consider k being Nat such that
A4: for x being set st x in rng M holds
ex q being FinSequence of D st
( x = q & len q = k ) by MATRIX_1:9;
consider p being FinSequence of D such that
A5: p in rng M and
A6: len p <> width M by A3;
reconsider x = p as set ;
A7: ex q being FinSequence of D st
( x = q & len q = k ) by A5, A4;
now__::_thesis:_len_p_=_width_M
percases ( n = 0 or n > 0 ) ;
suppose n = 0 ; ::_thesis: len p = width M
then  M = {} by A1;
hence  len p = width M by A5, RELAT_1:38; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: len p = width M
then consider s being FinSequence such that
A8: s in rng M and
A9: len s = width M by A1, MATRIX_1:def_3;
reconsider y = s as set ;
 ex r being FinSequence of D st
( y = r & len r = k ) by A4, A8;
hence  len p = width M by A7, A9; ::_thesis: verum
end;
end;
end;
hence  contradiction by A6; ::_thesis: verum
end;
end;
end;

begin

theorem Th8: :: MATRIX_2:8
for n, m being Nat
for D being non empty set
for M being Matrix of n,m,D
for k being Nat st k in Seg n holds
M . k = Line (M,k)
proof
let n, m be Nat; ::_thesis: for D being non empty set
for M being Matrix of n,m,D
for k being Nat st k in Seg n holds
M . k = Line (M,k)
let D be non empty set ; ::_thesis: for M being Matrix of n,m,D
for k being Nat st k in Seg n holds
M . k = Line (M,k)
let M be Matrix of n,m,D; ::_thesis: for k being Nat st k in Seg n holds
M . k = Line (M,k)
let k be Nat; ::_thesis: ( k in Seg n implies M . k = Line (M,k) )
assume A1: k in Seg n ; ::_thesis: M . k = Line (M,k)
 ( len M = n & dom M = Seg (len M) ) by FINSEQ_1:def_3, MATRIX_1:25;
then A2: M . k in rng M by A1, FUNCT_1:def_3;
percases ( n = 0 or 0 < n ) ;
suppose n = 0 ; ::_thesis: M . k = Line (M,k)
hence  M . k = Line (M,k) by A1; ::_thesis: verum
end;
supposeA3: 0 < n ; ::_thesis: M . k = Line (M,k)
consider l being Nat such that
A4: for x being set st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = l ) by MATRIX_1:9;
consider p being FinSequence of D such that
A5: M . k = p and
 len p = l by A2, A4;
A6: width M = m by A3, MATRIX_1:23;
A7: for j being Nat st j in Seg (width M) holds
p . j = M * (k,j)
proof
let j be Nat; ::_thesis: ( j in Seg (width M) implies p . j = M * (k,j) )
assume  j in Seg (width M) ; ::_thesis: p . j = M * (k,j)
then  [k,j] in [:(Seg n),(Seg m):] by A1, A6, ZFMISC_1:87;
then  [k,j] in Indices M by A3, MATRIX_1:23;
then  ex q being FinSequence of D st
( q = M . k & M * (k,j) = q . j ) by MATRIX_1:def_5;
hence  p . j = M * (k,j) by A5; ::_thesis: verum
end;
 len p = width M by A2, A6, A5, MATRIX_1:def_2;
hence  M . k = Line (M,k) by A5, A7, MATRIX_1:def_7; ::_thesis: verum
end;
end;
end;

Lm1:  for K being Field
for M being Matrix of K
for k being Nat st k in dom M holds
M . k = Line (M,k)
proof
let K be Field; ::_thesis: for M being Matrix of K
for k being Nat st k in dom M holds
M . k = Line (M,k)
let M be Matrix of K; ::_thesis: for k being Nat st k in dom M holds
M . k = Line (M,k)
let k be Nat; ::_thesis: ( k in dom M implies M . k = Line (M,k) )
assume A1: k in dom M ; ::_thesis: M . k = Line (M,k)
then  ( 1 <= k & k <= len M ) by FINSEQ_3:25;
then reconsider N = M as Matrix of len M, width M,K by MATRIX_1:20;
 k in Seg (len N) by A1, FINSEQ_1:def_3;
hence  M . k = Line (M,k) by Th8; ::_thesis: verum
end;

definition
let i be Nat;
let K be Field;
let M be Matrix of K;
func DelCol (M,i) ->  Matrix of K means :: MATRIX_2:def 5
( len it = len M & ( for k being Nat st k in dom M holds
it . k = Del ((Line (M,k)),i) ) );
existence
 ex b1 being Matrix of K st
( len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del ((Line (M,k)),i) ) )
proof
percases ( not i in Seg (width M) or i in Seg (width M) ) ;
supposeA1: not i in Seg (width M) ; ::_thesis: ex b1 being Matrix of K st
( len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del ((Line (M,k)),i) ) )
take  M ; ::_thesis: ( len M = len M & ( for k being Nat st k in dom M holds
M . k = Del ((Line (M,k)),i) ) )
thus  len M = len M ; ::_thesis: for k being Nat st k in dom M holds
M . k = Del ((Line (M,k)),i)
let k be Nat; ::_thesis: ( k in dom M implies M . k = Del ((Line (M,k)),i) )
assume A2: k in dom M ; ::_thesis: M . k = Del ((Line (M,k)),i)
 len (Line (M,k)) = width M by MATRIX_1:def_7;
then A3: not i in dom (Line (M,k)) by A1, FINSEQ_1:def_3;
thus M . k = Line (M,k) by A2, Lm1
.= Del ((Line (M,k)),i) by A3, FINSEQ_3:104 ; ::_thesis: verum
end;
supposeA4: i in Seg (width M) ; ::_thesis: ex b1 being Matrix of K st
( len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del ((Line (M,k)),i) ) )
defpred S1[ Nat, Nat, Element of K] means $3 = (Del ((Line (M,$1)),i)) . $2;
percases ( len M = 0 or len M > 0 ) ;
supposeA5: len M = 0 ; ::_thesis: ex b1 being Matrix of K st
( len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del ((Line (M,k)),i) ) )
then  Seg (len M) = {} ;
hence  ex b1 being Matrix of K st
( len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del ((Line (M,k)),i) ) ) by A4, A5, MATRIX_1:def_3; ::_thesis: verum
end;
supposeA6: len M > 0 ; ::_thesis: ex b1 being Matrix of K st
( len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del ((Line (M,k)),i) ) )
set n1 = width M;
percases ( width M = 0 or width M > 0 ) ;
suppose width M = 0 ; ::_thesis: ex b1 being Matrix of K st
( len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del ((Line (M,k)),i) ) )
hence  ex b1 being Matrix of K st
( len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del ((Line (M,k)),i) ) ) by A4; ::_thesis: verum
end;
suppose width M > 0 ; ::_thesis: ex b1 being Matrix of K st
( len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del ((Line (M,k)),i) ) )
then consider m being Nat such that
A7: width M = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
A8: for k being Nat st k in dom M holds
len (Del ((Line (M,k)),i)) = m
proof
let k be Nat; ::_thesis: ( k in dom M implies len (Del ((Line (M,k)),i)) = m )
assume  k in dom M ; ::_thesis: len (Del ((Line (M,k)),i)) = m
A9: len (Line (M,k)) = width M by MATRIX_1:def_7;
then  i in dom (Line (M,k)) by A4, FINSEQ_1:def_3;
then  ex l being Nat st
( len (Line (M,k)) = l + 1 & len (Del ((Line (M,k)),i)) = l ) by FINSEQ_3:104;
hence  len (Del ((Line (M,k)),i)) = m by A7, A9; ::_thesis: verum
end;
A10: for k, l being Nat st [k,l] in [:(Seg (len M)),(Seg m):] holds
ex x being Element of K st S1[k,l,x]
proof
let k, l be Nat; ::_thesis: ( [k,l] in [:(Seg (len M)),(Seg m):] implies ex x being Element of K st S1[k,l,x] )
assume A11: [k,l] in [:(Seg (len M)),(Seg m):] ; ::_thesis: ex x being Element of K st S1[k,l,x]
reconsider p = Del ((Line (M,k)),i) as FinSequence of K by FINSEQ_3:105;
 dom M = Seg (len M) by FINSEQ_1:def_3;
then  k in dom M by A11, ZFMISC_1:87;
then A12: len p = m by A8;
A13: dom p = Seg (len p) by FINSEQ_1:def_3;
 l in Seg m by A11, ZFMISC_1:87;
then reconsider x = p . l as Element of the carrier of K by A12, A13, FINSEQ_2:11;
take  x ; ::_thesis: S1[k,l,x]
thus  S1[k,l,x] ; ::_thesis: verum
end;
consider N being Matrix of len M,m,K such that
A14: for k, l being Nat st [k,l] in Indices N holds
S1[k,l,N * (k,l)] from MATRIX_1:sch_2(A10);
 dom M = Seg (len M) by FINSEQ_1:def_3;
then A15: Indices N = [:(dom M),(Seg m):] by A6, MATRIX_1:23;
A16: for k, l being Nat st k in dom M & l in Seg m holds
N * (k,l) = (Del ((Line (M,k)),i)) . l
proof
let k, l be Nat; ::_thesis: ( k in dom M & l in Seg m implies N * (k,l) = (Del ((Line (M,k)),i)) . l )
assume  ( k in dom M & l in Seg m ) ; ::_thesis: N * (k,l) = (Del ((Line (M,k)),i)) . l
then  [k,l] in Indices N by A15, ZFMISC_1:87;
hence  N * (k,l) = (Del ((Line (M,k)),i)) . l by A14; ::_thesis: verum
end;
A17: width N = m by A6, MATRIX_1:23;
reconsider N = N as Matrix of K ;
take  N ; ::_thesis: ( len N = len M & ( for k being Nat st k in dom M holds
N . k = Del ((Line (M,k)),i) ) )
 for k being Nat st k in dom M holds
N . k = Del ((Line (M,k)),i)
proof
let k be Nat; ::_thesis: ( k in dom M implies N . k = Del ((Line (M,k)),i) )
assume A18: k in dom M ; ::_thesis: N . k = Del ((Line (M,k)),i)
then  k in Seg (len M) by FINSEQ_1:def_3;
then A19: N . k = Line (N,k) by Th8;
reconsider s = N . k as FinSequence ;
A20: len s = m by A17, A19, MATRIX_1:def_7;
then A21: dom s = Seg m by FINSEQ_1:def_3;
A22: now__::_thesis:_for_j_being_Nat_st_j_in_dom_s_holds_
s_._j_=_(Del_((Line_(M,k)),i))_._j
let j be Nat; ::_thesis: ( j in dom s implies s . j = (Del ((Line (M,k)),i)) . j )
assume A23: j in dom s ; ::_thesis: s . j = (Del ((Line (M,k)),i)) . j
then  (Line (N,k)) . j = N * (k,j) by A17, A21, MATRIX_1:def_7;
hence  s . j = (Del ((Line (M,k)),i)) . j by A16, A18, A19, A21, A23; ::_thesis: verum
end;
 len (Del ((Line (M,k)),i)) = m by A8, A18;
hence  N . k = Del ((Line (M,k)),i) by A20, A22, FINSEQ_2:9; ::_thesis: verum
end;
hence  ( len N = len M & ( for k being Nat st k in dom M holds
N . k = Del ((Line (M,k)),i) ) ) by A6, MATRIX_1:23; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
uniqueness
 for b1, b2 being Matrix of K st len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del ((Line (M,k)),i) ) & len b2 = len M & ( for k being Nat st k in dom M holds
b2 . k = Del ((Line (M,k)),i) ) holds
b1 = b2
proof
let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M & ( for k being Nat st k in dom M holds
M1 . k = Del ((Line (M,k)),i) ) & len M2 = len M & ( for k being Nat st k in dom M holds
M2 . k = Del ((Line (M,k)),i) ) implies M1 = M2 )
assume that
A24: len M1 = len M and
A25: for k being Nat st k in dom M holds
M1 . k = Del ((Line (M,k)),i) and
A26: len M2 = len M and
A27: for k being Nat st k in dom M holds
M2 . k = Del ((Line (M,k)),i) ; ::_thesis: M1 = M2
A28: dom M1 = dom M by A24, FINSEQ_3:29;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_M1_holds_
M1_._k_=_M2_._k
let k be Nat; ::_thesis: ( k in dom M1 implies M1 . k = M2 . k )
assume A29: k in dom M1 ; ::_thesis: M1 . k = M2 . k
hence M1 . k = Del ((Line (M,k)),i) by A25, A28
.= M2 . k by A27, A28, A29 ;
::_thesis: verum
end;
hence  M1 = M2 by A24, A26, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem  defines DelCol MATRIX_2:def_5_:_
 for i being Nat
for K being Field
for M, b4 being Matrix of K holds
( b4 = DelCol (M,i) iff ( len b4 = len M & ( for k being Nat st k in dom M holds
b4 . k = Del ((Line (M,k)),i) ) ) );

theorem Th9: :: MATRIX_2:9
for D being non empty set
for M1, M2 being Matrix of D st M1 @ = M2 @ & len M1 = len M2 holds
M1 = M2
proof
let D be non empty set ; ::_thesis: for M1, M2 being Matrix of D st M1 @ = M2 @ & len M1 = len M2 holds
M1 = M2
let M1, M2 be Matrix of D; ::_thesis: ( M1 @ = M2 @ & len M1 = len M2 implies M1 = M2 )
assume that
A1: M1 @ = M2 @ and
A2: len M1 = len M2 ; ::_thesis: M1 = M2
 len (M1 @) = width M1 by MATRIX_1:def_6;
then A3: width M1 = width M2 by A1, MATRIX_1:def_6;
A4: Indices M2 = [:(dom M2),(Seg (width M2)):] ;
 for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A5: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
dom M1 = Seg (len M2) by A2, FINSEQ_1:def_3
.= dom M2 by FINSEQ_1:def_3 ;
then  (M2 @) * (j,i) = M2 * (i,j) by A3, A4, A5, MATRIX_1:def_6;
hence  M1 * (i,j) = M2 * (i,j) by A1, A5, MATRIX_1:def_6; ::_thesis: verum
end;
hence  M1 = M2 by A2, A3, MATRIX_1:21; ::_thesis: verum
end;

theorem Th10: :: MATRIX_2:10
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 MATRIX_1:def_6; ::_thesis: width (M @) = len M
percases ( len M = 0 or len M > 0 ) ;
suppose len M = 0 ; ::_thesis: width (M @) = len M
hence  width (M @) = len M by A1, MATRIX_1:def_3; ::_thesis: verum
end;
supposeA2: 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 A3: [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 Nat ;
 [i,j] in Indices (M @) by A3;
then  [j,i] in Indices M by MATRIX_1:def_6;
hence  [i,j] in [:(Seg (width M)),(dom M):] by ZFMISC_1:88; ::_thesis: verum
end;
assume A4: [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 Nat ;
 [j,i] in Indices M by A4, ZFMISC_1:88;
then  [i,j] in Indices (M @) by MATRIX_1:def_6;
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, A2, ZFMISC_1:110;
hence  width (M @) = len M by FINSEQ_1:def_3; ::_thesis: verum
end;
end;
end;

theorem :: MATRIX_2:11
for D being non empty set
for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 & M1 @ = M2 @ holds
M1 = M2
proof
let D be non empty set ; ::_thesis: for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 & M1 @ = M2 @ holds
M1 = M2
let M1, M2 be Matrix of D; ::_thesis: ( width M1 > 0 & width M2 > 0 & M1 @ = M2 @ implies M1 = M2 )
assume  ( width M1 > 0 & width M2 > 0 ) ; ::_thesis: ( not M1 @ = M2 @ or M1 = M2 )
then A1: ( width (M1 @) = len M1 & width (M2 @) = len M2 ) by Th10;
assume  M1 @ = M2 @ ; ::_thesis: M1 = M2
hence  M1 = M2 by A1, Th9; ::_thesis: verum
end;

theorem :: MATRIX_2:12
for D being non empty set
for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 holds
( M1 = M2 iff ( M1 @ = M2 @ & width M1 = width M2 ) )
proof
let D be non empty set ; ::_thesis: for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 holds
( M1 = M2 iff ( M1 @ = M2 @ & width M1 = width M2 ) )
let M1, M2 be Matrix of D; ::_thesis: ( width M1 > 0 & width M2 > 0 implies ( M1 = M2 iff ( M1 @ = M2 @ & width M1 = width M2 ) ) )
assume that
A1: width M1 > 0 and
A2: width M2 > 0 ; ::_thesis: ( M1 = M2 iff ( M1 @ = M2 @ & width M1 = width M2 ) )
thus  ( M1 = M2 implies ( M1 @ = M2 @ & width M1 = width M2 ) ) ; ::_thesis: ( M1 @ = M2 @ & width M1 = width M2 implies M1 = M2 )
assume that
A3: M1 @ = M2 @ and
A4: width M1 = width M2 ; ::_thesis: M1 = M2
 len M1 = width (M1 @) by A1, Th10;
then A5: len M1 = len M2 by A2, A3, Th10;
A6: Indices M2 = [:(dom M2),(Seg (width M2)):] ;
 for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A7: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
dom M1 = Seg (len M2) by A5, FINSEQ_1:def_3
.= dom M2 by FINSEQ_1:def_3 ;
then  (M2 @) * (j,i) = M2 * (i,j) by A4, A6, A7, MATRIX_1:def_6;
hence  M1 * (i,j) = M2 * (i,j) by A3, A7, MATRIX_1:def_6; ::_thesis: verum
end;
hence  M1 = M2 by A4, A5, MATRIX_1:21; ::_thesis: verum
end;

theorem Th13: :: MATRIX_2:13
for D being non empty set
for M being Matrix of D st len M > 0 & width M > 0 holds
(M @) @ = M
proof
let D be non empty set ; ::_thesis: for M being Matrix of D st len M > 0 & width M > 0 holds
(M @) @ = M
let M be Matrix of D; ::_thesis: ( len M > 0 & width M > 0 implies (M @) @ = M )
assume that
A1: len M > 0 and
A2: width M > 0 ; ::_thesis: (M @) @ = M
set N = M @ ;
A3: width (M @) = len M by A2, Th10;
A4: len ((M @) @) = width (M @) by MATRIX_1:def_6;
A5: len (M @) = width M by MATRIX_1:def_6;
 ( dom M = Seg (len M) & dom ((M @) @) = Seg (len ((M @) @)) ) by FINSEQ_1:def_3;
then A6: Indices ((M @) @) = Indices M by A1, A5, A3, A4, Th10;
A7: for i, j being Nat st [i,j] in Indices ((M @) @) holds
((M @) @) * (i,j) = M * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((M @) @) implies ((M @) @) * (i,j) = M * (i,j) )
assume A8: [i,j] in Indices ((M @) @) ; ::_thesis: ((M @) @) * (i,j) = M * (i,j)
then  [j,i] in Indices (M @) by MATRIX_1:def_6;
then  ((M @) @) * (i,j) = (M @) * (j,i) by MATRIX_1:def_6;
hence  ((M @) @) * (i,j) = M * (i,j) by A6, A8, MATRIX_1:def_6; ::_thesis: verum
end;
 width (M @) > 0 by A1, A2, Th10;
then  width ((M @) @) = width M by A5, Th10;
hence  (M @) @ = M by A3, A4, A7, MATRIX_1:21; ::_thesis: verum
end;

theorem Th14: :: MATRIX_2:14
for D being non empty set
for M being Matrix of D
for i being Nat st i in dom M holds
Line (M,i) = Col ((M @),i)
proof
let D be non empty set ; ::_thesis: for M being Matrix of D
for i being Nat st i in dom M holds
Line (M,i) = Col ((M @),i)
let M be Matrix of D; ::_thesis: for i being Nat st i in dom M holds
Line (M,i) = Col ((M @),i)
let i be Nat; ::_thesis: ( i in dom M implies Line (M,i) = Col ((M @),i) )
A1: len (M @) = width M by MATRIX_1:def_6;
 len (Col ((M @),i)) = len (M @) by MATRIX_1:def_8;
then A2: len (Col ((M @),i)) = width M by MATRIX_1:def_6;
then A3: dom (Col ((M @),i)) = Seg (width M) by FINSEQ_1:def_3;
assume A4: i in dom M ; ::_thesis: Line (M,i) = Col ((M @),i)
A5: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(Col_((M_@),i))_holds_
(Line_(M,i))_._j_=_(Col_((M_@),i))_._j
let j be Nat; ::_thesis: ( j in dom (Col ((M @),i)) implies (Line (M,i)) . j = (Col ((M @),i)) . j )
A6: dom (M @) = Seg (len (M @)) by FINSEQ_1:def_3;
assume A7: j in dom (Col ((M @),i)) ; ::_thesis: (Line (M,i)) . j = (Col ((M @),i)) . j
then  ( (Line (M,i)) . j = M * (i,j) & [i,j] in Indices M ) by A4, A3, MATRIX_1:def_7, ZFMISC_1:87;
hence (Line (M,i)) . j = (M @) * (j,i) by MATRIX_1:def_6
.= (Col ((M @),i)) . j by A1, A3, A7, A6, MATRIX_1:def_8 ;
::_thesis: verum
end;
 len (Line (M,i)) = width M by MATRIX_1:def_7;
hence  Line (M,i) = Col ((M @),i) by A2, A5, FINSEQ_2:9; ::_thesis: verum
end;

theorem :: MATRIX_2:15
for D being non empty set
for M being Matrix of D
for j being Nat st j in Seg (width M) holds
Line ((M @),j) = Col (M,j)
proof
let D be non empty set ; ::_thesis: for M being Matrix of D
for j being Nat st j in Seg (width M) holds
Line ((M @),j) = Col (M,j)
let M be Matrix of D; ::_thesis: for j being Nat st j in Seg (width M) holds
Line ((M @),j) = Col (M,j)
let j be Nat; ::_thesis: ( j in Seg (width M) implies Line ((M @),j) = Col (M,j) )
assume A1: j in Seg (width M) ; ::_thesis: Line ((M @),j) = Col (M,j)
then  j in Seg (len (M @)) by MATRIX_1:def_6;
then A2: j in dom (M @) by FINSEQ_1:def_3;
percases ( len M = 0 or len M > 0 ) ;
supposeA3: len M = 0 ; ::_thesis: Line ((M @),j) = Col (M,j)
then  Seg (len M) = {} ;
hence  Line ((M @),j) = Col (M,j) by A1, A3, MATRIX_1:def_3; ::_thesis: verum
end;
supposeA4: len M > 0 ; ::_thesis: Line ((M @),j) = Col (M,j)
percases ( width M = 0 or width M > 0 ) ;
suppose width M = 0 ; ::_thesis: Line ((M @),j) = Col (M,j)
hence  Line ((M @),j) = Col (M,j) by A1; ::_thesis: verum
end;
suppose width M > 0 ; ::_thesis: Line ((M @),j) = Col (M,j)
then  (M @) @ = M by A4, Th13;
hence  Line ((M @),j) = Col (M,j) by A2, Th14; ::_thesis: verum
end;
end;
end;
end;
end;

theorem :: MATRIX_2:16
for D being non empty set
for M being Matrix of D
for i being Nat st i in dom M holds
M . i = Line (M,i)
proof
let D be non empty set ; ::_thesis: for M being Matrix of D
for i being Nat st i in dom M holds
M . i = Line (M,i)
let M be Matrix of D; ::_thesis: for i being Nat st i in dom M holds
M . i = Line (M,i)
let i be Nat; ::_thesis: ( i in dom M implies M . i = Line (M,i) )
assume A1: i in dom M ; ::_thesis: M . i = Line (M,i)
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;
 M <> {} by A1;
then  M is Matrix of len M, width M,D by MATRIX_1:20;
then A3: len p = width M by A2, MATRIX_1:def_2;
A4: len (Line (M,i)) = width M by MATRIX_1:def_7;
then A5: dom (Line (M,i)) = Seg (width M) by FINSEQ_1:def_3;
A6: for j being Nat st j in Seg (width M) holds
M * (i,j) = p . j
proof
let j be Nat; ::_thesis: ( j in Seg (width M) implies M * (i,j) = p . j )
assume  j in Seg (width M) ; ::_thesis: M * (i,j) = p . j
then  [i,j] in Indices M by A1, ZFMISC_1:87;
then  ex q being FinSequence of D st
( q = M . i & q . j = M * (i,j) ) by MATRIX_1:def_5;
hence  M * (i,j) = p . j ; ::_thesis: verum
end;
now__::_thesis:_for_j_being_Nat_st_j_in_dom_(Line_(M,i))_holds_
(Line_(M,i))_._j_=_p_._j
let j be Nat; ::_thesis: ( j in dom (Line (M,i)) implies (Line (M,i)) . j = p . j )
assume A7: j in dom (Line (M,i)) ; ::_thesis: (Line (M,i)) . j = p . j
hence (Line (M,i)) . j = M * (i,j) by A5, MATRIX_1:def_7
.= p . j by A6, A5, A7 ;
::_thesis: verum
end;
hence  M . i = Line (M,i) by A3, A4, FINSEQ_2:9; ::_thesis: verum
end;

notation
let K be Field;
let i be Nat;
let M be Matrix of K;
synonym  DelLine (M,i) for  Del (i,K);
end;

registration
let K be Field;
let i be Nat;
let M be Matrix of K;
cluster DelLine (,M) ->  tabular ;
coherence
 DelLine (,M) is tabular
proof
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 MATRIX_1:def_1;
take  n ; :: according to MATRIX_1:def_1 ::_thesis: for b1 being set holds
( not b1 in rng (DelLine (,M)) or ex b2 being set st
( b2 = b1 & len b2 = n ) )
let x be set ; ::_thesis: ( not x in rng (DelLine (,M)) or ex b1 being set st
( b1 = x & len b1 = n ) )
A2: rng (DelLine (,M)) c= rng M by FINSEQ_3:106;
assume  x in rng (DelLine (,M)) ; ::_thesis: ex b1 being set st
( b1 = x & len b1 = n )
hence  ex b1 being set st
( b1 = x & len b1 = n ) by A1, A2; ::_thesis: verum
end;
end;

definition
let K be Field;
let i be Nat;
let M be Matrix of K;
:: original: DelLine
redefine func DelLine (M,i) ->  Matrix of K;
coherence
 DelLine (,M) is Matrix of K by FINSEQ_3:105;
end;

definition
let i, j, n be Nat;
let K be Field;
let M be Matrix of n,K;
func Deleting (M,i,j) ->  Matrix of K equals :: MATRIX_2:def 6
 DelCol ((DelLine (M,i)),j);
coherence
 DelCol ((DelLine (M,i)),j) is Matrix of K ;
end;

:: deftheorem  defines Deleting MATRIX_2:def_6_:_
 for i, j, n being Nat
for K being Field
for M being Matrix of n,K holds Deleting (M,i,j) = DelCol ((DelLine (M,i)),j);

begin

definition
let IT be set ;
attrIT is permutational  means :Def7: :: MATRIX_2:def 7
 ex n being Nat st
for x being set st x in IT holds
x is Permutation of (Seg n);
end;

:: deftheorem Def7 defines permutational MATRIX_2:def_7_:_
 for IT being set holds
( IT is permutational iff ex n being Nat st
for x being set st x in IT holds
x is Permutation of (Seg n) );

registration
cluster non empty permutational for set ;
existence
 ex b1 being set st
( b1 is permutational & not b1 is empty )
proof
set n = the Nat;
set p = the Permutation of (Seg the Nat);
take P = { the Permutation of (Seg the Nat)}; ::_thesis: ( P is permutational & not P is empty )
thus  P is permutational ::_thesis: not P is empty
proof
take  the Nat ; :: according to MATRIX_2:def_7 ::_thesis: for x being set st x in P holds
x is Permutation of (Seg the Nat)
let x be set ; ::_thesis: ( x in P implies x is Permutation of (Seg the Nat) )
assume  x in P ; ::_thesis: x is Permutation of (Seg the Nat)
hence  x is Permutation of (Seg the Nat) by TARSKI:def_1; ::_thesis: verum
end;
thus  not P is empty ; ::_thesis: verum
end;
end;

definition
let P be non empty permutational set ;
func len P ->  Nat means :Def8: :: MATRIX_2:def 8
 ex s being FinSequence st
( s in P & it = len s );
existence
 ex b1 being Nat ex s being FinSequence st
( s in P & b1 = len s )
proof
set x = the Element of P;
consider n being Nat such that
A1: for y being set st y in P holds
y is Permutation of (Seg n) by Def7;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
reconsider q = the Element of P as Permutation of (Seg n) by A1;
A2: dom q = Seg n by FUNCT_2:52;
then reconsider q = q as FinSequence by FINSEQ_1:def_2;
take  n ; ::_thesis: ex s being FinSequence st
( s in P & n = len s )
take  q ; ::_thesis: ( q in P & n = len q )
thus  ( q in P & n = len q ) by A2, FINSEQ_1:def_3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Nat st ex s being FinSequence st
( s in P & b1 = len s ) & ex s being FinSequence st
( s in P & b2 = len s ) holds
b1 = b2
proof
let n1, n2 be Nat; ::_thesis: ( ex s being FinSequence st
( s in P & n1 = len s ) & ex s being FinSequence st
( s in P & n2 = len s ) implies n1 = n2 )
given s1 being FinSequence such that A3: s1 in P and
A4: n1 = len s1 ; ::_thesis: ( for s being FinSequence holds
( not s in P or not n2 = len s ) or n1 = n2 )
consider n being Nat such that
A5: for y being set st y in P holds
y is Permutation of (Seg n) by Def7;
 s1 is Function of (Seg n),(Seg n) by A3, A5;
then  ( n in NAT & dom s1 = Seg n ) by FUNCT_2:52, ORDINAL1:def_12;
then A6: len s1 = n by FINSEQ_1:def_3;
given s2 being FinSequence such that A7: s2 in P and
A8: n2 = len s2 ; ::_thesis: n1 = n2
 s2 is Permutation of (Seg n) by A7, A5;
then  dom s2 = Seg n by FUNCT_2:52;
hence  n1 = n2 by A4, A8, A6, FINSEQ_1:def_3; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines len MATRIX_2:def_8_:_
 for P being non empty permutational set
for b2 being Nat holds
( b2 = len P iff ex s being FinSequence st
( s in P & b2 = len s ) );

definition
let P be non empty permutational set ;
:: original: len
redefine func len P ->  Element of NAT ;
coherence
 len P is Element of NAT by ORDINAL1:def_12;
end;

definition
let P be non empty permutational set ;
:: original: Element
redefine mode Element of P ->  Permutation of (Seg (len P));
coherence
 for b1 being Element of P holds b1 is Permutation of (Seg (len P))
proof
let x be Element of P; ::_thesis: x is Permutation of (Seg (len P))
consider n being Nat such that
A1: for y being set st y in P holds
y is Permutation of (Seg n) by Def7;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
reconsider q = x as Permutation of (Seg n) by A1;
A2: dom q = Seg n by FUNCT_2:52;
then reconsider q = q as FinSequence by FINSEQ_1:def_2;
 len q = n by A2, FINSEQ_1:def_3;
then  Seg (len P) = Seg n by Def8;
hence  x is Permutation of (Seg (len P)) by A1; ::_thesis: verum
end;
end;

theorem :: MATRIX_2:17
for n being Nat ex P being non empty permutational set st len P = n
proof
let n be Nat; ::_thesis: ex P being non empty permutational set st len P = n
set p = the Permutation of (Seg n);
set P = { the Permutation of (Seg n)};
now__::_thesis:_ex_n_being_Nat_st_
for_x_being_set_st_x_in_{_the_Permutation_of_(Seg_n)}_holds_
x_is_Permutation_of_(Seg_n)
take n = n; ::_thesis: for x being set st x in { the Permutation of (Seg n)} holds
x is Permutation of (Seg n)
let x be set ; ::_thesis: ( x in { the Permutation of (Seg n)} implies x is Permutation of (Seg n) )
assume  x in { the Permutation of (Seg n)} ; ::_thesis: x is Permutation of (Seg n)
hence  x is Permutation of (Seg n) by TARSKI:def_1; ::_thesis: verum
end;
then reconsider P = { the Permutation of (Seg n)} as non empty permutational set by Def7;
take  P ; ::_thesis: len P = n
 len P = n
proof
set x = the Element of P;
reconsider y = the Element of P as Function of (Seg n),(Seg n) by TARSKI:def_1;
A1: dom y = Seg n by FUNCT_2:52;
then reconsider s = y as FinSequence by FINSEQ_1:def_2;
 ( n in NAT & len P = len s ) by Def8, ORDINAL1:def_12;
hence  len P = n by A1, FINSEQ_1:def_3; ::_thesis: verum
end;
hence  len P = n ; ::_thesis: verum
end;

definition
let n be Nat;
func Permutations n ->  set  means :Def9: :: MATRIX_2:def 9
 for x being set holds
( x in it iff x is Permutation of (Seg n) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is Permutation of (Seg n) )
proof
defpred S1[ set ] means $1 is Permutation of (Seg n);
consider P being set  such that
A1: for x being set holds
( x in P iff ( x in Funcs ((Seg n),(Seg n)) & S1[x] ) ) from XBOOLE_0:sch_1();
take  P ; ::_thesis: for x being set holds
( x in P iff x is Permutation of (Seg n) )
let x be set ; ::_thesis: ( x in P iff x is Permutation of (Seg n) )
thus  ( x in P implies x is Permutation of (Seg n) ) by A1; ::_thesis: ( x is Permutation of (Seg n) implies x in P )
assume A2: x is Permutation of (Seg n) ; ::_thesis: x in P
then  x in Funcs ((Seg n),(Seg n)) by FUNCT_2:9;
hence  x in P by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Permutation of (Seg n) ) ) & ( for x being set holds
( x in b2 iff x is Permutation of (Seg n) ) ) holds
b1 = b2
proof
let P1, P2 be set ; ::_thesis: ( ( for x being set holds
( x in P1 iff x is Permutation of (Seg n) ) ) & ( for x being set holds
( x in P2 iff x is Permutation of (Seg n) ) ) implies P1 = P2 )
assume that
A3: for x being set holds
( x in P1 iff x is Permutation of (Seg n) ) and
A4: for x being set holds
( x in P2 iff x is Permutation of (Seg n) ) ; ::_thesis: P1 = P2
A5: now__::_thesis:_for_x_being_set_st_x_in_P2_holds_
x_in_P1
let x be set ; ::_thesis: ( x in P2 implies x in P1 )
assume  x in P2 ; ::_thesis: x in P1
then  x is Permutation of (Seg n) by A4;
hence  x in P1 by A3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_P1_holds_
x_in_P2
let x be set ; ::_thesis: ( x in P1 implies x in P2 )
assume  x in P1 ; ::_thesis: x in P2
then  x is Permutation of (Seg n) by A3;
hence  x in P2 by A4; ::_thesis: verum
end;
hence  P1 = P2 by A5, TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines Permutations MATRIX_2:def_9_:_
 for n being Nat
for b2 being set holds
( b2 = Permutations n iff for x being set holds
( x in b2 iff x is Permutation of (Seg n) ) );

registration
let n be Nat;
cluster Permutations n ->  non empty permutational ;
coherence
 ( Permutations n is permutational & not Permutations n is empty )
proof
defpred S1[ set ] means n is Permutation of (Seg n);
consider P being set  such that
A1: for x being set holds
( x in P iff ( x in Funcs ((Seg n),(Seg n)) & S1[x] ) ) from XBOOLE_0:sch_1();
 idseq n in Funcs ((Seg n),(Seg n)) by FUNCT_2:9;
then reconsider P = P as non empty set by A1;
now__::_thesis:_ex_n_being_Nat_st_
for_x_being_set_st_x_in_P_holds_
x_is_Permutation_of_(Seg_n)
take n = n; ::_thesis: for x being set st x in P holds
x is Permutation of (Seg n)
let x be set ; ::_thesis: ( x in P implies x is Permutation of (Seg n) )
assume  x in P ; ::_thesis: x is Permutation of (Seg n)
hence  x is Permutation of (Seg n) by A1; ::_thesis: verum
end;
then reconsider P = P as non empty permutational set by Def7;
 for x being set holds
( x in P iff x is Permutation of (Seg n) )
proof
let x be set ; ::_thesis: ( x in P iff x is Permutation of (Seg n) )
thus  ( x in P implies x is Permutation of (Seg n) ) by A1; ::_thesis: ( x is Permutation of (Seg n) implies x in P )
assume A2: x is Permutation of (Seg n) ; ::_thesis: x in P
then  x in Funcs ((Seg n),(Seg n)) by FUNCT_2:9;
hence  x in P by A1, A2; ::_thesis: verum
end;
hence  ( Permutations n is permutational & not Permutations n is empty ) by Def9; ::_thesis: verum
end;
end;

theorem :: MATRIX_2:18
for n being Nat holds len (Permutations n) = n
proof
let n be Nat; ::_thesis: len (Permutations n) = n
set x = the Element of Permutations n;
reconsider q = the Element of Permutations n as Permutation of (Seg n) by Def9;
A1: dom q = Seg n by FUNCT_2:52;
then reconsider q = q as FinSequence by FINSEQ_1:def_2;
 n in NAT by ORDINAL1:def_12;
then  len q = n by A1, FINSEQ_1:def_3;
hence  len (Permutations n) = n by Def8; ::_thesis: verum
end;

theorem :: MATRIX_2:19
Permutations 1 = {(idseq 1)}
proof
A1: Permutations 1 c= {(idseq 1)}
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Permutations 1 or p in {(idseq 1)} )
assume  p in Permutations 1 ; ::_thesis: p in {(idseq 1)}
then reconsider q = p as Permutation of (Seg 1) by Def9;
A2: dom q = Seg 1 by FUNCT_2:52;
 ( rng q = Seg 1 & 1 in {1} ) by FUNCT_2:def_3, TARSKI:def_1;
then  q . 1 in Seg 1 by FINSEQ_1:2, FUNCT_2:4;
then A3: q . 1 = 1 by FINSEQ_1:2, TARSKI:def_1;
reconsider q = q as FinSequence by A2, FINSEQ_1:def_2;
 len q = 1 by A2, FINSEQ_1:def_3;
then  q = idseq 1 by A3, FINSEQ_1:40, FINSEQ_2:50;
hence  p in {(idseq 1)} by TARSKI:def_1; ::_thesis: verum
end;
 {(idseq 1)} c= Permutations 1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(idseq 1)} or x in Permutations 1 )
assume  x in {(idseq 1)} ; ::_thesis: x in Permutations 1
then  x = idseq 1 by TARSKI:def_1;
hence  x in Permutations 1 by Def9; ::_thesis: verum
end;
hence  Permutations 1 = {(idseq 1)} by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

begin


definition
let n be Nat;
func Group_of_Perm n ->  strict multMagma  means :Def10: :: MATRIX_2:def 10
( the carrier of it = Permutations n & ( for q, p being Element of Permutations n holds the multF of it . (q,p) = p * q ) );
existence
 ex b1 being strict multMagma st
( the carrier of b1 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b1 . (q,p) = p * q ) )
proof
defpred S1[ Element of Permutations n, Element of Permutations n, set ] means $3 = $2 * $1;
A1: for q, p being Element of Permutations n ex z being Element of Permutations n st S1[q,p,z]
proof
let q, p be Element of Permutations n; ::_thesis: ex z being Element of Permutations n st S1[q,p,z]
reconsider p = p, q = q as Permutation of (Seg n) by Def9;
reconsider z = p * q as Element of Permutations n by Def9;
take  z ; ::_thesis: S1[q,p,z]
thus  S1[q,p,z] ; ::_thesis: verum
end;
consider o being BinOp of (Permutations n) such that
A2: for q, p being Element of Permutations n holds S1[q,p,o . (q,p)] from BINOP_1:sch_3(A1);
take  multMagma(# (Permutations n),o #) ; ::_thesis: ( the carrier of multMagma(# (Permutations n),o #) = Permutations n & ( for q, p being Element of Permutations n holds the multF of multMagma(# (Permutations n),o #) . (q,p) = p * q ) )
thus  ( the carrier of multMagma(# (Permutations n),o #) = Permutations n & ( for q, p being Element of Permutations n holds the multF of multMagma(# (Permutations n),o #) . (q,p) = p * q ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict multMagma st the carrier of b1 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b1 . (q,p) = p * q ) & the carrier of b2 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b2 . (q,p) = p * q ) holds
b1 = b2
proof
let G1, G2 be strict multMagma ; ::_thesis: ( the carrier of G1 = Permutations n & ( for q, p being Element of Permutations n holds the multF of G1 . (q,p) = p * q ) & the carrier of G2 = Permutations n & ( for q, p being Element of Permutations n holds the multF of G2 . (q,p) = p * q ) implies G1 = G2 )
assume that
A3: the carrier of G1 = Permutations n and
A4: for q, p being Element of Permutations n holds the multF of G1 . (q,p) = p * q and
A5: the carrier of G2 = Permutations n and
A6: for q, p being Element of Permutations n holds the multF of G2 . (q,p) = p * q ; ::_thesis: G1 = G2
now__::_thesis:_for_q,_p_being_Element_of_G1_holds_the_multF_of_G1_._(q,p)_=_the_multF_of_G2_._(q,p)
let q, p be Element of G1; ::_thesis: the multF of G1 . (q,p) = the multF of G2 . (q,p)
reconsider q9 = q, p9 = p as Element of Permutations n by A3;
thus  the multF of G1 . (q,p) = p9 * q9 by A4
.= the multF of G2 . (q,p) by A6 ; ::_thesis: verum
end;
hence  G1 = G2 by A3, A5, BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines Group_of_Perm MATRIX_2:def_10_:_
 for n being Nat
for b2 being strict multMagma holds
( b2 = Group_of_Perm n iff ( the carrier of b2 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b2 . (q,p) = p * q ) ) );

registration
let n be Nat;
cluster Group_of_Perm n ->  non empty strict ;
coherence
 not Group_of_Perm n is empty
proof
 the carrier of (Group_of_Perm n) = Permutations n by Def10;
hence  not the carrier of (Group_of_Perm n) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

theorem Th20: :: MATRIX_2:20
for n being Nat holds idseq n is Element of (Group_of_Perm n)
proof
let n be Nat; ::_thesis: idseq n is Element of (Group_of_Perm n)
 the carrier of (Group_of_Perm n) = Permutations n by Def10;
hence  idseq n is Element of (Group_of_Perm n) by Def9; ::_thesis: verum
end;

theorem Th21: :: MATRIX_2:21
for n being Nat
for p being Element of Permutations n holds
( p * (idseq n) = p & (idseq n) * p = p )
proof
let n be Nat; ::_thesis: for p being Element of Permutations n holds
( p * (idseq n) = p & (idseq n) * p = p )
let p be Element of Permutations n; ::_thesis: ( p * (idseq n) = p & (idseq n) * p = p )
A1: ( Seg n = {} implies Seg n = {} ) ;
 p is Permutation of (Seg n) by Def9;
then A2: rng p = Seg n by FUNCT_2:def_3;
 p is Function of (Seg n),(Seg n) by Def9;
then  dom p = Seg n by A1, FUNCT_2:def_1;
hence  ( p * (idseq n) = p & (idseq n) * p = p ) by A2, RELAT_1:52, RELAT_1:54; ::_thesis: verum
end;

theorem Th22: :: MATRIX_2:22
for n being Nat
for p being Element of Permutations n holds
( p * (p ") = idseq n & (p ") * p = idseq n )
proof
let n be Nat; ::_thesis: for p being Element of Permutations n holds
( p * (p ") = idseq n & (p ") * p = idseq n )
let p be Element of Permutations n; ::_thesis: ( p * (p ") = idseq n & (p ") * p = idseq n )
 p is Permutation of (Seg n) by Def9;
hence  ( p * (p ") = idseq n & (p ") * p = idseq n ) by FUNCT_2:61; ::_thesis: verum
end;

theorem Th23: :: MATRIX_2:23
for n being Nat
for p being Element of Permutations n holds p " is Element of (Group_of_Perm n)
proof
let n be Nat; ::_thesis: for p being Element of Permutations n holds p " is Element of (Group_of_Perm n)
let p be Element of Permutations n; ::_thesis: p " is Element of (Group_of_Perm n)
reconsider p = p as Permutation of (Seg n) by Def9;
 p " is Element of Permutations n by Def9;
hence  p " is Element of (Group_of_Perm n) by Def10; ::_thesis: verum
end;

registration
let n be Nat;
cluster Group_of_Perm n ->  strict Group-like associative ;
coherence
 ( Group_of_Perm n is associative & Group_of_Perm n is Group-like )
proof
A1: ex e being Element of (Group_of_Perm n) st
for p being Element of (Group_of_Perm n) holds
( p * e = p & e * p = p & ex g being Element of (Group_of_Perm n) st
( p * g = e & g * p = e ) )
proof
reconsider e = idseq n as Element of (Group_of_Perm n) by Th20;
take  e ; ::_thesis: for p being Element of (Group_of_Perm n) holds
( p * e = p & e * p = p & ex g being Element of (Group_of_Perm n) st
( p * g = e & g * p = e ) )
reconsider e9 = idseq n as Element of Permutations n by Def9;
A2: for p being Element of (Group_of_Perm n) ex g being Element of (Group_of_Perm n) st
( p * g = e & g * p = e )
proof
let p be Element of (Group_of_Perm n); ::_thesis: ex g being Element of (Group_of_Perm n) st
( p * g = e & g * p = e )
reconsider q = p as Element of Permutations n by Def10;
reconsider r = q as Permutation of (Seg n) by Def9;
reconsider f = r " as Element of Permutations n by Def9;
reconsider g = f as Element of (Group_of_Perm n) by Th23;
take  g ; ::_thesis: ( p * g = e & g * p = e )
A3: g * p = q * f by Def10
.= e by Th22 ;
p * g = f * q by Def10
.= e by Th22 ;
hence  ( p * g = e & g * p = e ) by A3; ::_thesis: verum
end;
 for p being Element of (Group_of_Perm n) holds
( p * e = p & e * p = p )
proof
let p be Element of (Group_of_Perm n); ::_thesis: ( p * e = p & e * p = p )
reconsider p9 = p as Element of Permutations n by Def10;
A4: e * p = p9 * e9 by Def10
.= p by Th21 ;
p * e = e9 * p9 by Def10
.= p by Th21 ;
hence  ( p * e = p & e * p = p ) by A4; ::_thesis: verum
end;
hence  for p being Element of (Group_of_Perm n) holds
( p * e = p & e * p = p & ex g being Element of (Group_of_Perm n) st
( p * g = e & g * p = e ) ) by A2; ::_thesis: verum
end;
 for p, q, r being Element of (Group_of_Perm n) holds (p * q) * r = p * (q * r)
proof
let p, q, r be Element of (Group_of_Perm n); ::_thesis: (p * q) * r = p * (q * r)
reconsider p9 = p, q9 = q, r9 = r as Element of Permutations n by Def10;
A5: ( q9 * p9 is Permutation of (Seg n) & r9 * q9 is Permutation of (Seg n) )
proof
reconsider p9 = p9, q9 = q9, r9 = r9 as Permutation of (Seg n) by Def9;
 ( q9 * p9 is Permutation of (Seg n) & r9 * q9 is Permutation of (Seg n) ) ;
hence  ( q9 * p9 is Permutation of (Seg n) & r9 * q9 is Permutation of (Seg n) ) ; ::_thesis: verum
end;
then A6: q9 * p9 is Element of Permutations n by Def9;
A7: r9 * q9 is Element of Permutations n by A5, Def9;
(p * q) * r = the multF of (Group_of_Perm n) . ((q9 * p9),r9) by Def10
.= r9 * (q9 * p9) by A6, Def10
.= (r9 * q9) * p9 by RELAT_1:36
.= the multF of (Group_of_Perm n) . (p9,(r9 * q9)) by A7, Def10
.= p * (q * r) by Def10 ;
hence  (p * q) * r = p * (q * r) ; ::_thesis: verum
end;
hence  ( Group_of_Perm n is associative & Group_of_Perm n is Group-like ) by A1, GROUP_1:1; ::_thesis: verum
end;
end;

theorem Th24: :: MATRIX_2:24
for n being Nat holds idseq n = 1_ (Group_of_Perm n)
proof
let n be Nat; ::_thesis: idseq n = 1_ (Group_of_Perm n)
reconsider e = idseq n as Element of (Group_of_Perm n) by Th20;
reconsider e9 = idseq n as Element of Permutations n by Def9;
 for p being Element of (Group_of_Perm n) holds
( p * e = p & e * p = p )
proof
let p be Element of (Group_of_Perm n); ::_thesis: ( p * e = p & e * p = p )
reconsider p9 = p as Element of Permutations n by Def10;
A1: e * p = p9 * e9 by Def10
.= p by Th21 ;
p * e = e9 * p9 by Def10
.= p by Th21 ;
hence  ( p * e = p & e * p = p ) by A1; ::_thesis: verum
end;
hence  idseq n = 1_ (Group_of_Perm n) by GROUP_1:4; ::_thesis: verum
end;

definition
let n be Nat;
let p be Permutation of (Seg n);
attrp is being_transposition  means :: MATRIX_2:def 11
 ex i, j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) );
end;

:: deftheorem  defines being_transposition MATRIX_2:def_11_:_
 for n being Nat
for p being Permutation of (Seg n) holds
( p is being_transposition iff ex i, j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) ) );

definition
let n be Nat;
let IT be Permutation of (Seg n);
attrIT is even  means :Def12: :: MATRIX_2:def 12
 ex l being FinSequence of (Group_of_Perm n) st
( (len l) mod 2 = 0 & IT = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) );
end;

:: deftheorem Def12 defines even MATRIX_2:def_12_:_
 for n being Nat
for IT being Permutation of (Seg n) holds
( IT is even iff ex l being FinSequence of (Group_of_Perm n) st
( (len l) mod 2 = 0 & IT = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) ) );

notation
let n be Nat;
let IT be Permutation of (Seg n);
antonym  odd IT for  even ;
end;

theorem :: MATRIX_2:25
for n being Nat holds id (Seg n) is even
proof
let n be Nat; ::_thesis: id (Seg n) is even
set l = <*> the carrier of (Group_of_Perm n);
 0 = (2 * 0) + 0 ;
then A1: (len (<*> the carrier of (Group_of_Perm n))) mod 2 = 0 by NAT_D:def_2;
 Product (<*> the carrier of (Group_of_Perm n)) = 1_ (Group_of_Perm n) by GROUP_4:8;
then A2: idseq n = Product (<*> the carrier of (Group_of_Perm n)) by Th24;
 for i being Nat st i in dom (<*> the carrier of (Group_of_Perm n)) holds
ex q being Element of Permutations n st
( (<*> the carrier of (Group_of_Perm n)) . i = q & q is being_transposition ) ;
hence  id (Seg n) is even by A1, A2, Def12; ::_thesis: verum
end;

definition
let K be Field;
let n be Nat;
let x be Element of K;
let p be Element of Permutations n;
func - (x,p) ->  Element of K equals :: MATRIX_2:def 13
x if p is even
otherwise  - x;
correctness
coherence
( ( p is even implies x is Element of K ) & ( not p is even implies - x is Element of K ) );
consistency
for b1 being Element of K holds verum;
;
end;

:: deftheorem  defines - MATRIX_2:def_13_:_
 for K being Field
for n being Nat
for x being Element of K
for p being Element of Permutations n holds
( ( p is even implies - (x,p) = x ) & ( not p is even implies - (x,p) = - x ) );

definition
let X be set ;
assume A1: X is finite ;
func FinOmega X ->  Element of Fin X equals :: MATRIX_2:def 14
X;
coherence
 X is Element of Fin X by A1, FINSUB_1:def_5;
end;

:: deftheorem  defines FinOmega MATRIX_2:def_14_:_
 for X being set st X is finite holds
FinOmega X = X;

theorem :: MATRIX_2:26
for n being Nat holds Permutations n is finite
proof
let n be Nat; ::_thesis: Permutations n is finite
A1: Permutations n c= Funcs ((Seg n),(Seg n))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Permutations n or x in Funcs ((Seg n),(Seg n)) )
assume  x in Permutations n ; ::_thesis: x in Funcs ((Seg n),(Seg n))
then  x is Function of (Seg n),(Seg n) by Def9;
hence  x in Funcs ((Seg n),(Seg n)) by FUNCT_2:9; ::_thesis: verum
end;
 Funcs ((Seg n),(Seg n)) is finite by FRAENKEL:6;
hence  Permutations n is finite by A1, FINSET_1:1; ::_thesis: verum
end;