:: MATRIX_7 semantic presentation

begin


theorem Th1: :: MATRIX_7:1
for f being Permutation of (Seg 2) holds
( f = <*1,2*> or f = <*2,1*> )
proof
let f be Permutation of (Seg 2); ::_thesis: ( f = <*1,2*> or f = <*2,1*> )
A1: rng f = Seg 2 by FUNCT_2:def_3;
 2 in {1,2} by TARSKI:def_2;
then A2: f . 2 in Seg 2 by A1, FINSEQ_1:2, FUNCT_2:4;
A3: dom f = Seg 2 by FUNCT_2:52;
then reconsider p = f as FinSequence by FINSEQ_1:def_2;
A4: len p = 2 by A3, FINSEQ_1:def_3;
A5: ( 1 in dom f & 2 in dom f ) by A3;
 1 in {1,2} by TARSKI:def_2;
then A6: f . 1 in Seg 2 by A1, FINSEQ_1:2, FUNCT_2:4;
now__::_thesis:_(_(_f_._1_=_1_&_f_._2_=_1_&_contradiction_)_or_(_f_._1_=_1_&_f_._2_=_2_&_(_f_=_<*1,2*>_or_f_=_<*2,1*>_)_)_or_(_f_._1_=_2_&_f_._2_=_1_&_(_f_=_<*1,2*>_or_f_=_<*2,1*>_)_)_or_(_f_._1_=_2_&_f_._2_=_2_&_contradiction_)_)
percases ( ( f . 1 = 1 & f . 2 = 1 ) or ( f . 1 = 1 & f . 2 = 2 ) or ( f . 1 = 2 & f . 2 = 1 ) or ( f . 1 = 2 & f . 2 = 2 ) ) by A6, A2, FINSEQ_1:2, TARSKI:def_2;
case ( f . 1 = 1 & f . 2 = 1 ) ; ::_thesis: contradiction
hence  contradiction by A5, FUNCT_1:def_4; ::_thesis: verum
end;
case ( f . 1 = 1 & f . 2 = 2 ) ; ::_thesis: ( f = <*1,2*> or f = <*2,1*> )
hence  ( f = <*1,2*> or f = <*2,1*> ) by A4, FINSEQ_1:44; ::_thesis: verum
end;
case ( f . 1 = 2 & f . 2 = 1 ) ; ::_thesis: ( f = <*1,2*> or f = <*2,1*> )
hence  ( f = <*1,2*> or f = <*2,1*> ) by A4, FINSEQ_1:44; ::_thesis: verum
end;
case ( f . 1 = 2 & f . 2 = 2 ) ; ::_thesis: contradiction
hence  contradiction by A5, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;
hence  ( f = <*1,2*> or f = <*2,1*> ) ; ::_thesis: verum
end;

theorem Th2: :: MATRIX_7:2
for f being FinSequence st ( f = <*1,2*> or f = <*2,1*> ) holds
f is Permutation of (Seg 2)
proof
let f be FinSequence; ::_thesis: ( ( f = <*1,2*> or f = <*2,1*> ) implies f is Permutation of (Seg 2) )
assume A1: ( f = <*1,2*> or f = <*2,1*> ) ; ::_thesis: f is Permutation of (Seg 2)
 ( len <*1,2*> = 2 & len <*2,1*> = 2 ) by FINSEQ_1:44;
then A2: dom f = Seg 2 by A1, FINSEQ_1:def_3;
 rng f c= Seg 2
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Seg 2 )
assume  y in rng f ; ::_thesis: y in Seg 2
then  ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
then  ( y = f . 1 or y = f . 2 ) by A2, FINSEQ_1:2, TARSKI:def_2;
then  ( y = 1 or y = 2 or y = 2 or y = 1 ) by A1, FINSEQ_1:44;
hence  y in Seg 2 ; ::_thesis: verum
end;
then reconsider g = f as Function of (Seg 2),(Seg 2) by A2, FUNCT_2:2;
now__::_thesis:_(_(_f_=_<*1,2*>_&_f_is_Permutation_of_(Seg_2)_)_or_(_f_=_<*2,1*>_&_f_is_Permutation_of_(Seg_2)_)_)
percases ( f = <*1,2*> or f = <*2,1*> ) by A1;
caseA3: f = <*1,2*> ; ::_thesis: f is Permutation of (Seg 2)
 for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A4: ( x1 in dom f & x2 in dom f ) and
A5: f . x1 = f . x2 ; ::_thesis: x1 = x2
now__::_thesis:_(_(_x1_=_1_&_x2_=_1_&_x1_=_x2_)_or_(_x1_=_1_&_x2_=_2_&_contradiction_)_or_(_x1_=_2_&_x2_=_1_&_contradiction_)_or_(_x1_=_2_&_x2_=_2_&_x1_=_x2_)_)
percases ( ( x1 = 1 & x2 = 1 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) or ( x1 = 2 & x2 = 2 ) ) by A2, A4, FINSEQ_1:2, TARSKI:def_2;
case ( x1 = 1 & x2 = 1 ) ; ::_thesis: x1 = x2
hence  x1 = x2 ; ::_thesis: verum
end;
caseA6: ( x1 = 1 & x2 = 2 ) ; ::_thesis: contradiction
then  f . x1 = 1 by A3, FINSEQ_1:44;
hence  contradiction by A3, A5, A6, FINSEQ_1:44; ::_thesis: verum
end;
caseA7: ( x1 = 2 & x2 = 1 ) ; ::_thesis: contradiction
then  f . x1 = 2 by A3, FINSEQ_1:44;
hence  contradiction by A3, A5, A7, FINSEQ_1:44; ::_thesis: verum
end;
case ( x1 = 2 & x2 = 2 ) ; ::_thesis: x1 = x2
hence  x1 = x2 ; ::_thesis: verum
end;
end;
end;
hence  x1 = x2 ; ::_thesis: verum
end;
then A8: f is one-to-one by FUNCT_1:def_4;
now__::_thesis:_for_x_being_set_st_x_in_rng_f_holds_
x_in_Seg_2
let x be set ; ::_thesis: ( x in rng f implies x in Seg 2 )
assume  x in rng f ; ::_thesis: x in Seg 2
then consider z being set  such that
A9: z in dom f and
A10: f . z = x by FUNCT_1:def_3;
 len f = 2 by A3, FINSEQ_1:44;
then  dom f = Seg 2 by FINSEQ_1:def_3;
then  ( z = 1 or z = 2 ) by A9, FINSEQ_1:2, TARSKI:def_2;
then  ( x = 1 or x = 2 ) by A3, A10, FINSEQ_1:44;
hence  x in Seg 2 ; ::_thesis: verum
end;
then A11: rng f c= Seg 2 by TARSKI:def_3;
 Seg 2 c= rng f
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Seg 2 or z in rng f )
assume  z in Seg 2 ; ::_thesis: z in rng f
then  ( z = 1 or z = 2 ) by FINSEQ_1:2, TARSKI:def_2;
then A12: ( z = f . 1 or z = f . 2 ) by A3, FINSEQ_1:44;
 ( 1 in dom f & 2 in dom f ) by A2;
hence  z in rng f by A12, FUNCT_1:def_3; ::_thesis: verum
end;
then  rng f = Seg 2 by A11, XBOOLE_0:def_10;
then  g is onto by FUNCT_2:def_3;
hence  f is Permutation of (Seg 2) by A8; ::_thesis: verum
end;
caseA13: f = <*2,1*> ; ::_thesis: f is Permutation of (Seg 2)
 for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A14: ( x1 in dom f & x2 in dom f ) and
A15: f . x1 = f . x2 ; ::_thesis: x1 = x2
now__::_thesis:_(_(_x1_=_1_&_x2_=_1_&_x1_=_x2_)_or_(_x1_=_1_&_x2_=_2_&_contradiction_)_or_(_x1_=_2_&_x2_=_1_&_contradiction_)_or_(_x1_=_2_&_x2_=_2_&_x1_=_x2_)_)
percases ( ( x1 = 1 & x2 = 1 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) or ( x1 = 2 & x2 = 2 ) ) by A2, A14, FINSEQ_1:2, TARSKI:def_2;
case ( x1 = 1 & x2 = 1 ) ; ::_thesis: x1 = x2
hence  x1 = x2 ; ::_thesis: verum
end;
caseA16: ( x1 = 1 & x2 = 2 ) ; ::_thesis: contradiction
then  f . x1 = 2 by A13, FINSEQ_1:44;
hence  contradiction by A13, A15, A16, FINSEQ_1:44; ::_thesis: verum
end;
caseA17: ( x1 = 2 & x2 = 1 ) ; ::_thesis: contradiction
then  f . x1 = 1 by A13, FINSEQ_1:44;
hence  contradiction by A13, A15, A17, FINSEQ_1:44; ::_thesis: verum
end;
case ( x1 = 2 & x2 = 2 ) ; ::_thesis: x1 = x2
hence  x1 = x2 ; ::_thesis: verum
end;
end;
end;
hence  x1 = x2 ; ::_thesis: verum
end;
then A18: f is one-to-one by FUNCT_1:def_4;
now__::_thesis:_for_x_being_set_st_x_in_rng_f_holds_
x_in_Seg_2
let x be set ; ::_thesis: ( x in rng f implies x in Seg 2 )
assume  x in rng f ; ::_thesis: x in Seg 2
then consider z being set  such that
A19: z in dom f and
A20: f . z = x by FUNCT_1:def_3;
 len f = 2 by A13, FINSEQ_1:44;
then  dom f = Seg 2 by FINSEQ_1:def_3;
then  ( z = 1 or z = 2 ) by A19, FINSEQ_1:2, TARSKI:def_2;
then  ( x = 2 or x = 1 ) by A13, A20, FINSEQ_1:44;
hence  x in Seg 2 ; ::_thesis: verum
end;
then A21: rng f c= Seg 2 by TARSKI:def_3;
 Seg 2 c= rng f
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Seg 2 or z in rng f )
assume  z in Seg 2 ; ::_thesis: z in rng f
then  ( z = 1 or z = 2 ) by FINSEQ_1:2, TARSKI:def_2;
then A22: ( z = f . 2 or z = f . 1 ) by A13, FINSEQ_1:44;
 ( 2 in dom f & 1 in dom f ) by A2;
hence  z in rng f by A22, FUNCT_1:def_3; ::_thesis: verum
end;
then  rng f = Seg 2 by A21, XBOOLE_0:def_10;
then  g is onto by FUNCT_2:def_3;
hence  f is Permutation of (Seg 2) by A18; ::_thesis: verum
end;
end;
end;
hence  f is Permutation of (Seg 2) ; ::_thesis: verum
end;

theorem Th3: :: MATRIX_7:3
Permutations 2 = {<*1,2*>,<*2,1*>}
proof
now__::_thesis:_for_x_being_set_st_x_in_{(idseq_2),<*2,1*>}_holds_
x_in_Permutations_2
let x be set ; ::_thesis: ( x in {(idseq 2),<*2,1*>} implies x in Permutations 2 )
assume A1: x in {(idseq 2),<*2,1*>} ; ::_thesis: x in Permutations 2
now__::_thesis:_(_(_x_=_idseq_2_&_x_in_Permutations_2_)_or_(_x_=_<*2,1*>_&_x_in_Permutations_2_)_)
percases ( x = idseq 2 or x = <*2,1*> ) by A1, TARSKI:def_2;
case x = idseq 2 ; ::_thesis: x in Permutations 2
hence  x in Permutations 2 by MATRIX_2:def_9; ::_thesis: verum
end;
caseA2: x = <*2,1*> ; ::_thesis: x in Permutations 2
 <*2,1*> is Permutation of (Seg 2) by Th2;
hence  x in Permutations 2 by A2, MATRIX_2:def_9; ::_thesis: verum
end;
end;
end;
hence  x in Permutations 2 ; ::_thesis: verum
end;
then A3: {(idseq 2),<*2,1*>} c= Permutations 2 by TARSKI:def_3;
now__::_thesis:_for_p_being_set_st_p_in_Permutations_2_holds_
p_in_{(idseq_2),<*2,1*>}
let p be set ; ::_thesis: ( p in Permutations 2 implies p in {(idseq 2),<*2,1*>} )
assume  p in Permutations 2 ; ::_thesis: p in {(idseq 2),<*2,1*>}
then reconsider q = p as Permutation of (Seg 2) by MATRIX_2:def_9;
 ( q = <*1,2*> or q = <*2,1*> ) by Th1;
hence  p in {(idseq 2),<*2,1*>} by FINSEQ_2:52, TARSKI:def_2; ::_thesis: verum
end;
then  Permutations 2 c= {(idseq 2),<*2,1*>} by TARSKI:def_3;
hence  Permutations 2 = {<*1,2*>,<*2,1*>} by A3, FINSEQ_2:52, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th4: :: MATRIX_7:4
for p being Permutation of (Seg 2) st p is being_transposition holds
p = <*2,1*>
proof
let p be Permutation of (Seg 2); ::_thesis: ( p is being_transposition implies p = <*2,1*> )
assume A1: p is being_transposition ; ::_thesis: p = <*2,1*>
now__::_thesis:_not_p_=_<*1,2*>
set p0 = <*1,2*>;
assume A2: p = <*1,2*> ; ::_thesis: contradiction
consider i, j being Nat such that
A3: i in dom p and
A4: ( j in dom p & i <> j ) and
A5: p . i = j and
 p . j = i and
 for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k by A1, MATRIX_2:def_11;
 len <*1,2*> = 2 by FINSEQ_1:44;
then A6: dom p = {1,2} by A2, FINSEQ_1:2, FINSEQ_1:def_3;
then A7: ( i = 1 or i = 2 ) by A3, TARSKI:def_2;
now__::_thesis:_(_(_i_=_1_&_j_=_2_&_contradiction_)_or_(_i_=_2_&_j_=_1_&_contradiction_)_)
percases ( ( i = 1 & j = 2 ) or ( i = 2 & j = 1 ) ) by A4, A6, A7, TARSKI:def_2;
case ( i = 1 & j = 2 ) ; ::_thesis: contradiction
hence  contradiction by A2, A5, FINSEQ_1:44; ::_thesis: verum
end;
case ( i = 2 & j = 1 ) ; ::_thesis: contradiction
hence  contradiction by A2, A5, FINSEQ_1:44; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
hence  p = <*2,1*> by Th1; ::_thesis: verum
end;

theorem Th5: :: MATRIX_7:5
for D being non empty set
for f being FinSequence of D
for k2 being Element of NAT st 1 <= k2 & k2 < len f holds
f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f)))
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for k2 being Element of NAT st 1 <= k2 & k2 < len f holds
f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f)))
let f be FinSequence of D; ::_thesis: for k2 being Element of NAT st 1 <= k2 & k2 < len f holds
f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f)))
let k2 be Element of NAT ; ::_thesis: ( 1 <= k2 & k2 < len f implies f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f))) )
assume A1: ( 1 <= k2 & k2 < len f ) ; ::_thesis: f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f)))
then  mid (f,1,(len f)) = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f))) by INTEGRA2:4;
hence  f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f))) by A1, FINSEQ_6:120, XXREAL_0:2; ::_thesis: verum
end;

theorem Th6: :: MATRIX_7:6
for D being non empty set
for f being FinSequence of D st 2 <= len f holds
f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f)))
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D st 2 <= len f holds
f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f)))
let f be FinSequence of D; ::_thesis: ( 2 <= len f implies f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f))) )
assume A1: 2 <= len f ; ::_thesis: f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f)))
then A2: (len f) -' 2 = (len f) - 2 by XREAL_1:233;
then A3: ((len f) -' 2) + 1 = (((len f) - 1) - 1) + 1
.= (len f) -' 1 by A1, XREAL_1:233, XXREAL_0:2 ;
now__::_thesis:_(_(_(len_f)_-'_2_>_0_&_f_=_(f_|_((len_f)_-'_2))_^_(mid_(f,((len_f)_-'_1),(len_f)))_)_or_(_(len_f)_-'_2_=_0_&_f_=_(f_|_((len_f)_-'_2))_^_(mid_(f,((len_f)_-'_1),(len_f)))_)_)
percases ( (len f) -' 2 > 0 or (len f) -' 2 = 0 ) ;
case (len f) -' 2 > 0 ; ::_thesis: f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f)))
then A4: 0 + 1 <= (len f) -' 2 by NAT_1:13;
 len f < (len f) + 1 by NAT_1:13;
then  len f < ((len f) + 1) + 1 by NAT_1:13;
then  (len f) - 2 < ((len f) + 2) - 2 by XREAL_1:14;
then  f = (mid (f,1,((len f) -' 2))) ^ (mid (f,(((len f) -' 2) + 1),(len f))) by A2, A4, Th5;
hence  f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f))) by A3, A4, FINSEQ_6:116; ::_thesis: verum
end;
caseA5: (len f) -' 2 = 0 ; ::_thesis: f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f)))
then A6: mid (f,(((len f) -' 2) + 1),(len f)) = f by A1, FINSEQ_6:120, XXREAL_0:2;
A7: f | 0 is empty ;
((len f) -' 2) + 1 = ((len f) - 2) + 1 by A1, XREAL_1:233
.= (len f) - 1
.= (len f) -' 1 by A1, XREAL_1:233, XXREAL_0:2 ;
hence  f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f))) by A5, A6, A7, FINSEQ_1:34; ::_thesis: verum
end;
end;
end;
hence  f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f))) ; ::_thesis: verum
end;

theorem Th7: :: MATRIX_7:7
for D being non empty set
for f being FinSequence of D st 1 <= len f holds
f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f)))
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D st 1 <= len f holds
f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f)))
let f be FinSequence of D; ::_thesis: ( 1 <= len f implies f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f))) )
assume A1: 1 <= len f ; ::_thesis: f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f)))
then A2: (len f) -' 1 = (len f) - 1 by XREAL_1:233;
now__::_thesis:_(_(_(len_f)_-'_1_>_0_&_f_=_(f_|_((len_f)_-'_1))_^_(mid_(f,(len_f),(len_f)))_)_or_(_(len_f)_-'_1_=_0_&_f_=_(f_|_((len_f)_-'_1))_^_(mid_(f,(len_f),(len_f)))_)_)
percases ( (len f) -' 1 > 0 or (len f) -' 1 = 0 ) ;
case (len f) -' 1 > 0 ; ::_thesis: f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f)))
then A3: 0 + 1 <= (len f) -' 1 by NAT_1:13;
 len f < (len f) + 1 by NAT_1:13;
then  (len f) - 1 < ((len f) + 1) - 1 by XREAL_1:14;
then  f = (mid (f,1,((len f) -' 1))) ^ (mid (f,(((len f) -' 1) + 1),(len f))) by A2, A3, Th5;
hence  f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f))) by A2, A3, FINSEQ_6:116; ::_thesis: verum
end;
caseA4: (len f) -' 1 = 0 ; ::_thesis: f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f)))
A5: f | 0 is empty ;
 mid (f,(((len f) -' 1) + 1),(len f)) = f by A1, A4, FINSEQ_6:120;
hence  f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f))) by A2, A4, A5, FINSEQ_1:34; ::_thesis: verum
end;
end;
end;
hence  f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f))) ; ::_thesis: verum
end;

Lm1:  <*1,2*> <> <*2,1*>
by FINSEQ_1:77;

theorem Th8: :: MATRIX_7:8
for a being Element of (Group_of_Perm 2) st ex q being Element of Permutations 2 st
( q = a & q is being_transposition ) holds
a = <*2,1*>
proof
let a be Element of (Group_of_Perm 2); ::_thesis: ( ex q being Element of Permutations 2 st
( q = a & q is being_transposition ) implies a = <*2,1*> )
given q being Element of Permutations 2 such that A1: q = a and
A2: q is being_transposition ; ::_thesis: a = <*2,1*>
 the carrier of (Group_of_Perm 2) = Permutations 2 by MATRIX_2:def_10;
then reconsider b = a as Permutation of (Seg 2) by MATRIX_2:def_9;
 ex i, j being Nat st
( i in dom q & j in dom q & i <> j & q . i = j & q . j = i & ( for k being Nat st k <> i & k <> j & k in dom q holds
q . k = k ) ) by A2, MATRIX_2:def_11;
then  b is being_transposition by A1, MATRIX_2:def_11;
hence  a = <*2,1*> by Th4; ::_thesis: verum
end;

theorem :: MATRIX_7:9
for n being Element of NAT
for a, b being Element of (Group_of_Perm n)
for pa, pb being Element of Permutations n st a = pa & b = pb holds
a * b = pb * pa by MATRIX_2:def_10;

theorem Th10: :: MATRIX_7:10
for a, b being Element of (Group_of_Perm 2) st ex p being Element of Permutations 2 st
( p = a & p is being_transposition ) & ex q being Element of Permutations 2 st
( q = b & q is being_transposition ) holds
a * b = <*1,2*>
proof
let a, b be Element of (Group_of_Perm 2); ::_thesis: ( ex p being Element of Permutations 2 st
( p = a & p is being_transposition ) & ex q being Element of Permutations 2 st
( q = b & q is being_transposition ) implies a * b = <*1,2*> )
assume that
A1: ex p being Element of Permutations 2 st
( p = a & p is being_transposition ) and
A2: ex q being Element of Permutations 2 st
( q = b & q is being_transposition ) ; ::_thesis: a * b = <*1,2*>
consider p being Element of Permutations 2 such that
A3: p = a and
A4: p is being_transposition by A1;
 the carrier of (Group_of_Perm 2) = Permutations 2 by MATRIX_2:def_10;
then A5: ( a * b = <*1,2*> or a * b = <*2,1*> ) by Th3, TARSKI:def_2;
reconsider p2 = p as FinSequence by A3, A4, Th8;
A6: a = <*2,1*> by A1, Th8;
then  len p2 = 2 by A3, FINSEQ_1:44;
then  1 in Seg (len p2) ;
then A7: 1 in dom p2 by FINSEQ_1:def_3;
consider q being Element of Permutations 2 such that
A8: q = b and
A9: q is being_transposition by A2;
reconsider q2 = q as FinSequence by A8, A9, Th8;
 b = <*2,1*> by A2, Th8;
then A10: q2 . 2 = 1 by A8, FINSEQ_1:44;
A11: a * b = q * p by A3, A8, MATRIX_2:def_10;
 p2 . 1 = 2 by A6, A3, FINSEQ_1:44;
then  (q * p) . 1 = 1 by A10, A7, FUNCT_1:13;
hence  a * b = <*1,2*> by A5, A11, FINSEQ_1:44; ::_thesis: verum
end;

theorem Th11: :: MATRIX_7:11
for l being FinSequence of (Group_of_Perm 2) st (len l) mod 2 = 0 & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 2 st
( l . i = q & q is being_transposition ) ) holds
Product l = <*1,2*>
proof
defpred S1[ Element of NAT ] means  for f being FinSequence of (Group_of_Perm 2) st len f = 2 * $1 & ( for i being Nat st i in dom f holds
ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) ) holds
Product f = <*1,2*>;
let l be FinSequence of (Group_of_Perm 2); ::_thesis: ( (len l) mod 2 = 0 & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 2 st
( l . i = q & q is being_transposition ) ) implies Product l = <*1,2*> )
assume that
A1: (len l) mod 2 = 0 and
A2: for i being Nat st i in dom l holds
ex q being Element of Permutations 2 st
( l . i = q & q is being_transposition ) ; ::_thesis: Product l = <*1,2*>
 ( ex t being Nat st
( len l = (2 * t) + 0 & 0 < 2 ) or ( 0 = 0 & 2 = 0 ) ) by A1, NAT_D:def_2;
then consider t being Nat such that
A3: len l = 2 * t ;
A4: for s being Element of NAT st S1[s] holds
S1[s + 1]
proof
let s be Element of NAT ; ::_thesis: ( S1[s] implies S1[s + 1] )
assume A5: S1[s] ; ::_thesis: S1[s + 1]
 for f being FinSequence of (Group_of_Perm 2) st len f = 2 * (s + 1) & ( for i being Nat st i in dom f holds
ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) ) holds
Product f = <*1,2*>
proof
let f be FinSequence of (Group_of_Perm 2); ::_thesis: ( len f = 2 * (s + 1) & ( for i being Nat st i in dom f holds
ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) ) implies Product f = <*1,2*> )
assume that
A6: len f = 2 * (s + 1) and
A7: for i being Nat st i in dom f holds
ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) ; ::_thesis: Product f = <*1,2*>
A8: len f = (2 * s) + 2 by A6;
then A9: 2 <= len f by NAT_1:11;
then A10: (len f) -' 1 = (len f) - 1 by XREAL_1:233, XXREAL_0:2;
A11: ((len f) - ((len f) -' 1)) + 1 = ((len f) - ((len f) - 1)) + 1 by A9, XREAL_1:233, XXREAL_0:2
.= 2 ;
set g = mid (f,((len f) -' 1),(len f));
A12: (len f) -' 1 <= len f by NAT_D:35;
A13: 1 <= len f by A9, XXREAL_0:2;
then  len f in Seg (len f) ;
then  len f in dom f by FINSEQ_1:def_3;
then A14: ex q being Element of Permutations 2 st
( f . (len f) = q & q is being_transposition ) by A7;
reconsider pw2 = Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) as Element of (Group_of_Perm 2) ;
reconsider pw1 = Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) as Element of (Group_of_Perm 2) ;
A15: (1 + ((len f) -' 1)) -' 1 = (1 + ((len f) -' 1)) - 1 by NAT_1:11, XREAL_1:233
.= (len f) -' 1 ;
A16: (1 + 1) - 1 <= (len f) - 1 by A9, XREAL_1:13;
then A17: 1 <= (len f) -' 1 by A9, XREAL_1:233, XXREAL_0:2;
then A18: len (mid (f,((len f) -' 1),(len f))) = ((len f) -' ((len f) -' 1)) + 1 by A13, A12, FINSEQ_6:118
.= ((len f) - ((len f) -' 1)) + 1 by NAT_D:35, XREAL_1:233
.= ((len f) - ((len f) - 1)) + 1 by A9, XREAL_1:233, XXREAL_0:2
.= 2 ;
then  (len (mid (f,((len f) -' 1),(len f)))) -' 1 = (len (mid (f,((len f) -' 1),(len f)))) - 1 by XREAL_1:233;
then A19: ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) . 1 = (mid (f,((len f) -' 1),(len f))) . 1 by A18, FINSEQ_3:112
.= f . ((len f) -' 1) by A16, A12, A11, A15, FINSEQ_6:122 ;
A20: for i being Nat st i in dom (f | ((len f) -' 2)) holds
ex q being Element of Permutations 2 st
( (f | ((len f) -' 2)) . i = q & q is being_transposition )
proof
let i be Nat; ::_thesis: ( i in dom (f | ((len f) -' 2)) implies ex q being Element of Permutations 2 st
( (f | ((len f) -' 2)) . i = q & q is being_transposition ) )
assume  i in dom (f | ((len f) -' 2)) ; ::_thesis: ex q being Element of Permutations 2 st
( (f | ((len f) -' 2)) . i = q & q is being_transposition )
then A21: i in Seg (len (f | ((len f) -' 2))) by FINSEQ_1:def_3;
then A22: 1 <= i by FINSEQ_1:1;
A23: i <= len (f | ((len f) -' 2)) by A21, FINSEQ_1:1;
 len (f | ((len f) -' 2)) <= len f by FINSEQ_5:16;
then  i <= len f by A23, XXREAL_0:2;
then  i in dom f by A22, FINSEQ_3:25;
then A24: ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) by A7;
 len (f | ((len f) -' 2)) = (len f) -' 2 by FINSEQ_1:59, NAT_D:35;
hence  ex q being Element of Permutations 2 st
( (f | ((len f) -' 2)) . i = q & q is being_transposition ) by A23, A24, FINSEQ_3:112; ::_thesis: verum
end;
len (f | ((len f) -' 2)) = (len f) -' 2 by FINSEQ_1:59, NAT_D:35
.= 2 * s by A8, NAT_D:34 ;
then  Product (f | ((len f) -' 2)) = <*1,2*> by A5, A20;
then A25: 1_ (Group_of_Perm 2) = Product (f | ((len f) -' 2)) by FINSEQ_2:52, MATRIX_2:24;
 f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f))) by A8, Th6, NAT_1:11;
then A26: Product f = (Product (f | ((len f) -' 2))) * (Product (mid (f,((len f) -' 1),(len f)))) by GROUP_4:5
.= Product (mid (f,((len f) -' 1),(len f))) by A25, GROUP_1:def_4 ;
 2 <= 2 + ((len f) -' 1) by NAT_1:11;
then A27: (2 + ((len f) -' 1)) -' 1 = (2 + ((len f) -' 1)) - 1 by XREAL_1:233, XXREAL_0:2
.= len f by A10 ;
A28: ((len f) - ((len f) -' 1)) + 1 = ((len f) - ((len f) - 1)) + 1 by A9, XREAL_1:233, XXREAL_0:2
.= 1 + 1 ;
A29: (1 + (len (mid (f,((len f) -' 1),(len f))))) -' 1 = (1 + (len (mid (f,((len f) -' 1),(len f))))) - 1 by NAT_1:11, XREAL_1:233;
A30: len ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) = (len (mid (f,((len f) -' 1),(len f)))) -' 1 by FINSEQ_1:59, NAT_D:35
.= (len (mid (f,((len f) -' 1),(len f)))) - 1 by A18, XREAL_1:233
.= 1 by A18 ;
then  1 in Seg (len ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))) ;
then  1 in dom ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) by FINSEQ_1:def_3;
then  ( rng ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) c= the carrier of (Group_of_Perm 2) & ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) . 1 in rng ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) ) by FINSEQ_1:def_4, FUNCT_1:def_3;
then reconsider r = ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) . 1 as Element of (Group_of_Perm 2) ;
A31: pw1 = Product <*r*> by A30, FINSEQ_1:40
.= f . ((len f) -' 1) by A19, FINSOP_1:11 ;
 1 <= ((len (mid (f,((len f) -' 1),(len f)))) - (len (mid (f,((len f) -' 1),(len f))))) + 1 ;
then A32: (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) . 1 = (mid (f,((len f) -' 1),(len f))) . ((1 + (len (mid (f,((len f) -' 1),(len f))))) -' 1) by A18, FINSEQ_6:122
.= f . (len f) by A16, A12, A18, A28, A29, A27, FINSEQ_6:122 ;
A33: len (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) = ((len (mid (f,((len f) -' 1),(len f)))) -' (len (mid (f,((len f) -' 1),(len f))))) + 1 by A18, FINSEQ_6:118
.= 0 + 1 by XREAL_1:232
.= 1 ;
then  1 in Seg (len (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f))))))) ;
then  1 in dom (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) by FINSEQ_1:def_3;
then  ( rng (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) c= the carrier of (Group_of_Perm 2) & (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) . 1 in rng (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) ) by FINSEQ_1:def_4, FUNCT_1:def_3;
then reconsider s = (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) . 1 as Element of (Group_of_Perm 2) ;
A34: pw2 = Product <*s*> by A33, FINSEQ_1:40
.= f . (len f) by A32, FINSOP_1:11 ;
 (len f) -' 1 in Seg (len f) by A17, A12;
then  (len f) -' 1 in dom f by FINSEQ_1:def_3;
then A35: ex q being Element of Permutations 2 st
( f . ((len f) -' 1) = q & q is being_transposition ) by A7;
 mid (f,((len f) -' 1),(len f)) = ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) ^ (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) by A18, Th7;
then  Product (mid (f,((len f) -' 1),(len f))) = (Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))) * (Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f))))))) by GROUP_4:5
.= <*1,2*> by A35, A14, A31, A34, Th10 ;
hence  Product f = <*1,2*> by A26; ::_thesis: verum
end;
hence  S1[s + 1] ; ::_thesis: verum
end;
 for f being FinSequence of (Group_of_Perm 2) st len f = 2 * 0 & ( for i being Nat st i in dom f holds
ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) ) holds
Product f = <*1,2*>
proof
set G = Group_of_Perm 2;
let f be FinSequence of (Group_of_Perm 2); ::_thesis: ( len f = 2 * 0 & ( for i being Nat st i in dom f holds
ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) ) implies Product f = <*1,2*> )
assume that
A36: len f = 2 * 0 and
 for i being Nat st i in dom f holds
ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) ; ::_thesis: Product f = <*1,2*>
A37: 1_ (Group_of_Perm 2) = <*1,2*> by FINSEQ_2:52, MATRIX_2:24;
 f = <*> the carrier of (Group_of_Perm 2) by A36;
hence  Product f = <*1,2*> by A37, GROUP_4:8; ::_thesis: verum
end;
then A38: S1[ 0 ] ;
A39: for s being Element of NAT holds S1[s] from NAT_1:sch_1(A38, A4);
reconsider t = t as Element of NAT by ORDINAL1:def_12;
 len l = 2 * t by A3;
hence  Product l = <*1,2*> by A2, A39; ::_thesis: verum
end;

theorem :: MATRIX_7:12
for K being Field
for M being Matrix of 2,K holds Det M = ((M * (1,1)) * (M * (2,2))) - ((M * (1,2)) * (M * (2,1)))
proof
reconsider s1 = <*1,2*>, s2 = <*2,1*> as Permutation of (Seg 2) by Th2;
let K be Field; ::_thesis: for M being Matrix of 2,K holds Det M = ((M * (1,1)) * (M * (2,2))) - ((M * (1,2)) * (M * (2,1)))
let M be Matrix of 2,K; ::_thesis: Det M = ((M * (1,1)) * (M * (2,2))) - ((M * (1,2)) * (M * (2,1)))
A1: now__::_thesis:_not_s1_=_s2
A2: s1 . 1 = 1 by FINSEQ_1:44;
assume  s1 = s2 ; ::_thesis: contradiction
hence  contradiction by A2, FINSEQ_1:44; ::_thesis: verum
end;
set D0 = {s1,s2};
reconsider l0 = <*> {s1,s2} as FinSequence of (Group_of_Perm 2) by Th3, MATRIX_2:def_10;
set X = Permutations 2;
reconsider p1 = s1, p2 = s2 as Element of Permutations 2 by MATRIX_2:def_9;
set Y = the carrier of K;
set f = Path_product M;
set F = the addF of K;
set di = the multF of K $$ (Path_matrix (p1,M));
set B = FinOmega (Permutations 2);
A3: FinOmega (Permutations 2) = Permutations 2 by MATRIX_2:26, MATRIX_2:def_14;
 Det M = the addF of K $$ ((FinOmega (Permutations 2)),(Path_product M)) by MATRIX_3:def_9;
then consider G being Function of (Fin (Permutations 2)), the carrier of K such that
A4: Det M = G . (FinOmega (Permutations 2)) and
 for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G . {} = e and
A5: for x being Element of Permutations 2 holds G . {x} = (Path_product M) . x and
A6: for B9 being Element of Fin (Permutations 2) st B9 c= FinOmega (Permutations 2) & B9 <> {} holds
for x being Element of Permutations 2 st x in (FinOmega (Permutations 2)) \ B9 holds
G . (B9 \/ {x}) = the addF of K . ((G . B9),((Path_product M) . x)) by A3, SETWISEO:def_3;
A7: G . {p1} = (Path_product M) . p1 by A5;
A8: G . (FinOmega (Permutations 2)) = the addF of K . (((Path_product M) . p1),((Path_product M) . p2))
proof
reconsider B9 = {.p1.} as Element of Fin (Permutations 2) ;
A9: B9 c= FinOmega (Permutations 2)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in B9 or y in FinOmega (Permutations 2) )
assume  y in B9 ; ::_thesis: y in FinOmega (Permutations 2)
then  y = p1 by TARSKI:def_1;
hence  y in FinOmega (Permutations 2) by A3; ::_thesis: verum
end;
 (FinOmega (Permutations 2)) \ B9 = {s2} by A1, A3, Th3, ZFMISC_1:17;
then  s2 in (FinOmega (Permutations 2)) \ B9 by TARSKI:def_1;
then  G . (B9 \/ {p2}) = the addF of K . ((G . B9),((Path_product M) . p2)) by A6, A9;
hence  G . (FinOmega (Permutations 2)) = the addF of K . (((Path_product M) . p1),((Path_product M) . p2)) by A3, A7, Th3, ENUMSET1:1; ::_thesis: verum
end;
set dj = the multF of K $$ (Path_matrix (p2,M));
A10: p1 . 2 = 2 by FINSEQ_1:44;
A11: p2 . 2 = 1 by FINSEQ_1:44;
A12: len (Path_matrix (p1,M)) = 2 by MATRIX_3:def_7;
then consider f3 being Function of NAT, the carrier of K such that
A13: f3 . 1 = (Path_matrix (p1,M)) . 1 and
A14: for n being Element of NAT st 0 <> n & n < 2 holds
f3 . (n + 1) = the multF of K . ((f3 . n),((Path_matrix (p1,M)) . (n + 1))) and
A15: the multF of K $$ (Path_matrix (p1,M)) = f3 . 2 by FINSOP_1:def_1;
A16: 1 in Seg 2 ;
then A17: 1 in dom (Path_matrix (p1,M)) by A12, FINSEQ_1:def_3;
A18: 2 in Seg 2 ;
then  2 in dom (Path_matrix (p1,M)) by A12, FINSEQ_1:def_3;
then A19: ( p1 . 1 = 1 & (Path_matrix (p1,M)) . 2 = M * (2,2) ) by A10, FINSEQ_1:44, MATRIX_3:def_7;
A20: len (Path_matrix (p2,M)) = 2 by MATRIX_3:def_7;
then consider f4 being Function of NAT, the carrier of K such that
A21: f4 . 1 = (Path_matrix (p2,M)) . 1 and
A22: for n being Element of NAT st 0 <> n & n < 2 holds
f4 . (n + 1) = the multF of K . ((f4 . n),((Path_matrix (p2,M)) . (n + 1))) and
A23: the multF of K $$ (Path_matrix (p2,M)) = f4 . 2 by FINSOP_1:def_1;
A24: 1 in dom (Path_matrix (p2,M)) by A20, A16, FINSEQ_1:def_3;
 2 in dom (Path_matrix (p2,M)) by A20, A18, FINSEQ_1:def_3;
then A25: ( p2 . 1 = 2 & (Path_matrix (p2,M)) . 2 = M * (2,1) ) by A11, FINSEQ_1:44, MATRIX_3:def_7;
A26: f4 . (1 + 1) = the multF of K . ((f4 . 1),((Path_matrix (p2,M)) . (1 + 1))) by A22
.= (M * (1,2)) * (M * (2,1)) by A24, A25, A21, MATRIX_3:def_7 ;
A27: len (Permutations 2) = 2 by MATRIX_2:18;
 for l being FinSequence of (Group_of_Perm 2) holds
( not (len l) mod 2 = 0 or not s2 = Product l or ex i being Nat st
( i in dom l & ( for q being Element of Permutations 2 holds
( not l . i = q or not q is being_transposition ) ) ) ) by Lm1, Th11;
then  ( (Path_product M) . p2 = - (( the multF of K "**" (Path_matrix (p2,M))),p2) & p2 is odd ) by A27, MATRIX_2:def_12, MATRIX_3:def_8;
then A28: (Path_product M) . p2 = - ( the multF of K $$ (Path_matrix (p2,M))) by MATRIX_2:def_13;
A29: Product l0 = Product (<*> the carrier of (Group_of_Perm 2))
.= 1_ (Group_of_Perm 2) by GROUP_4:8
.= p1 by FINSEQ_2:52, MATRIX_2:24 ;
A30: 0 mod 2 = 0 by NAT_D:26;
 ex l being FinSequence of (Group_of_Perm 2) st
( (len l) mod 2 = 0 & s1 = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 2 st
( l . i = q & q is being_transposition ) ) )
proof
take  l0 ; ::_thesis: ( (len l0) mod 2 = 0 & s1 = Product l0 & ( for i being Nat st i in dom l0 holds
ex q being Element of Permutations 2 st
( l0 . i = q & q is being_transposition ) ) )
thus  ( (len l0) mod 2 = 0 & s1 = Product l0 ) by A30, A29; ::_thesis: for i being Nat st i in dom l0 holds
ex q being Element of Permutations 2 st
( l0 . i = q & q is being_transposition )
let i be Nat; ::_thesis: ( i in dom l0 implies ex q being Element of Permutations 2 st
( l0 . i = q & q is being_transposition ) )
thus  ( i in dom l0 implies ex q being Element of Permutations 2 st
( l0 . i = q & q is being_transposition ) ) ; ::_thesis: verum
end;
then A31: ( (Path_product M) . p1 = - (( the multF of K "**" (Path_matrix (p1,M))),p1) & p1 is even ) by A27, MATRIX_2:def_12, MATRIX_3:def_8;
f3 . (1 + 1) = the multF of K . ((f3 . 1),((Path_matrix (p1,M)) . (1 + 1))) by A14
.= (M * (1,1)) * (M * (2,2)) by A17, A19, A13, MATRIX_3:def_7 ;
hence  Det M = ((M * (1,1)) * (M * (2,2))) - ((M * (1,2)) * (M * (2,1))) by A4, A8, A15, A23, A26, A31, A28, MATRIX_2:def_13; ::_thesis: verum
end;

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
let a be Element of K;
:: original: *
redefine funca * M ->  Matrix of n,K;
coherence
 a * M is Matrix of n,K
proof
A1: width (a * M) = width M by MATRIX_3:def_5;
A2: len M = n by MATRIX_1:def_2;
A3: len (a * M) = len M by MATRIX_3:def_5;
A4: len M = n by MATRIX_1:def_2;
now__::_thesis:_(_(_len_M_>_0_&_a_*_M_is_Matrix_of_n,K_)_or_(_len_M_<=_0_&_a_*_M_is_Matrix_of_n,K_)_)
percases ( len M > 0 or len M <= 0 ) ;
caseA5: len M > 0 ; ::_thesis: a * M is Matrix of n,K
then  n = width M by A2, MATRIX_1:20;
hence  a * M is Matrix of n,K by A2, A3, A1, A5, MATRIX_1:20; ::_thesis: verum
end;
case len M <= 0 ; ::_thesis: a * M is Matrix of n,K
then A6: len (a * M) = 0 by MATRIX_3:def_5;
then A7: Seg (len (a * M)) = {} ;
 for p being FinSequence of K st p in rng (a * M) holds
len p = 0
proof
let p be FinSequence of K; ::_thesis: ( p in rng (a * M) implies len p = 0 )
assume  p in rng (a * M) ; ::_thesis: len p = 0
then  ex x being set st
( x in dom (a * M) & p = (a * M) . x ) by FUNCT_1:def_3;
hence  len p = 0 by A7, FINSEQ_1:def_3; ::_thesis: verum
end;
hence  a * M is Matrix of n,K by A4, A3, A6, MATRIX_1:def_2; ::_thesis: verum
end;
end;
end;
hence  a * M is Matrix of n,K ; ::_thesis: verum
end;
end;

theorem Th13: :: MATRIX_7:13
for K being Field
for n, m being Element of NAT holds
( len (0. (K,n,m)) = n & dom (0. (K,n,m)) = Seg n )
proof
let K be Field; ::_thesis: for n, m being Element of NAT holds
( len (0. (K,n,m)) = n & dom (0. (K,n,m)) = Seg n )
let n, m be Element of NAT ; ::_thesis: ( len (0. (K,n,m)) = n & dom (0. (K,n,m)) = Seg n )
 len (n |-> (m |-> (0. K))) = n by CARD_1:def_7;
hence  len (0. (K,n,m)) = n by MATRIX_3:def_1; ::_thesis: dom (0. (K,n,m)) = Seg n
hence  dom (0. (K,n,m)) = Seg n by FINSEQ_1:def_3; ::_thesis: verum
end;

theorem Th14: :: MATRIX_7:14
for K being Field
for n being Element of NAT
for p being Element of Permutations n
for i being Element of NAT st i in Seg n holds
p . i in Seg n
proof
let K be Field; ::_thesis: for n being Element of NAT
for p being Element of Permutations n
for i being Element of NAT st i in Seg n holds
p . i in Seg n
let n be Element of NAT ; ::_thesis: for p being Element of Permutations n
for i being Element of NAT st i in Seg n holds
p . i in Seg n
let p be Element of Permutations n; ::_thesis: for i being Element of NAT st i in Seg n holds
p . i in Seg n
let i be Element of NAT ; ::_thesis: ( i in Seg n implies p . i in Seg n )
A1: p is Permutation of (Seg n) by MATRIX_2:def_9;
assume  i in Seg n ; ::_thesis: p . i in Seg n
hence  p . i in Seg n by A1, FUNCT_2:5; ::_thesis: verum
end;

theorem :: MATRIX_7:15
for K being Field
for n being Element of NAT st n >= 1 holds
Det (0. (K,n,n)) = 0. K
proof
let K be Field; ::_thesis: for n being Element of NAT st n >= 1 holds
Det (0. (K,n,n)) = 0. K
let n be Element of NAT ; ::_thesis: ( n >= 1 implies Det (0. (K,n,n)) = 0. K )
set B = FinOmega (Permutations n);
set f = Path_product (0. (K,n,n));
set F = the addF of K;
set Y = the carrier of K;
set X = Permutations n;
reconsider G0 = (Fin (Permutations n)) --> (0. K) as Function of (Fin (Permutations n)), the carrier of K ;
A1: G0 . (FinOmega (Permutations n)) = 0. K by FUNCOP_1:7;
A2: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G0 . {} = e
proof
let e be Element of the carrier of K; ::_thesis: ( e is_a_unity_wrt the addF of K implies G0 . {} = e )
 0. K is_a_unity_wrt the addF of K by FVSUM_1:6;
then A3: the addF of K . ((0. K),e) = e by BINOP_1:3;
assume  e is_a_unity_wrt the addF of K ; ::_thesis: G0 . {} = e
then  the addF of K . ((0. K),e) = 0. K by BINOP_1:3;
hence  G0 . {} = e by A3, FINSUB_1:7, FUNCOP_1:7; ::_thesis: verum
end;
assume A4: n >= 1 ; ::_thesis: Det (0. (K,n,n)) = 0. K
A5: for x being set st x in dom (Path_product (0. (K,n,n))) holds
(Path_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x
proof
let x be set ; ::_thesis: ( x in dom (Path_product (0. (K,n,n))) implies (Path_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x )
assume  x in dom (Path_product (0. (K,n,n))) ; ::_thesis: (Path_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x
 for p being Element of Permutations n holds ((Permutations n) --> (0. K)) . p = - (( the multF of K $$ (Path_matrix (p,(0. (K,n,n))))),p)
proof
defpred S1[ Element of NAT ] means  the multF of K $$ (($1 + 1) |-> (0. K)) = 0. K;
let p be Element of Permutations n; ::_thesis: ((Permutations n) --> (0. K)) . p = - (( the multF of K $$ (Path_matrix (p,(0. (K,n,n))))),p)
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A7: ((k + 1) + 1) |-> (0. K) = ((k + 1) |-> (0. K)) ^ <*(0. K)*> by FINSEQ_2:60;
assume  S1[k] ; ::_thesis: S1[k + 1]
then  the multF of K $$ (((k + 1) + 1) |-> (0. K)) = (0. K) * (0. K) by A7, FINSOP_1:4
.= 0. K by VECTSP_1:6 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
 1 |-> (0. K) = <*(0. K)*> by FINSEQ_2:59;
then A8: S1[ 0 ] by FINSOP_1:11;
A9: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A8, A6);
A10: now__::_thesis:_(_(_p_is_even_&_-_((0._K),p)_=_0._K_)_or_(_not_p_is_even_&_-_((0._K),p)_=_0._K_)_)
percases ( p is even or not p is even ) ;
case p is even ; ::_thesis: - ((0. K),p) = 0. K
hence  - ((0. K),p) = 0. K by MATRIX_2:def_13; ::_thesis: verum
end;
case not p is even ; ::_thesis: - ((0. K),p) = 0. K
then  - ((0. K),p) = - (0. K) by MATRIX_2:def_13
.= 0. K by RLVECT_1:12 ;
hence  - ((0. K),p) = 0. K ; ::_thesis: verum
end;
end;
end;
A11: for i, j being Nat st i in dom (n |-> (0. K)) & j = p . i holds
(n |-> (0. K)) . i = (0. (K,n,n)) * (i,j)
proof
let i, j be Nat; ::_thesis: ( i in dom (n |-> (0. K)) & j = p . i implies (n |-> (0. K)) . i = (0. (K,n,n)) * (i,j) )
assume that
A12: i in dom (n |-> (0. K)) and
A13: j = p . i ; ::_thesis: (n |-> (0. K)) . i = (0. (K,n,n)) * (i,j)
A14: i in Seg n by A12, FUNCOP_1:13;
then  j in Seg n by A13, Th14;
then A15: j in Seg (width (0. (K,n,n))) by A4, MATRIX_1:23;
 i in dom (0. (K,n,n)) by A14, Th13;
then A16: [i,j] in Indices (0. (K,n,n)) by A15, ZFMISC_1:def_2;
 (n |-> (0. K)) . i = 0. K by A14, FUNCOP_1:7;
hence  (n |-> (0. K)) . i = (0. (K,n,n)) * (i,j) by A16, MATRIX_3:1; ::_thesis: verum
end;
 len (n |-> (0. K)) = n by CARD_1:def_7;
then A17: Path_matrix (p,(0. (K,n,n))) = n |-> (0. K) by A11, MATRIX_3:def_7;
 n -' 1 = n - 1 by A4, XREAL_1:233;
then A18: (n -' 1) + 1 = n ;
 ((Permutations n) --> (0. K)) . p = 0. K by FUNCOP_1:7;
hence  ((Permutations n) --> (0. K)) . p = - (( the multF of K $$ (Path_matrix (p,(0. (K,n,n))))),p) by A17, A9, A18, A10; ::_thesis: verum
end;
hence  (Path_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x by MATRIX_3:def_8; ::_thesis: verum
end;
 dom ((Permutations n) --> (0. K)) = Permutations n by FUNCOP_1:13;
then  dom (Path_product (0. (K,n,n))) = dom ((Permutations n) --> (0. K)) by FUNCT_2:def_1;
then A19: Path_product (0. (K,n,n)) = (Permutations n) --> (0. K) by A5, FUNCT_1:2;
A20: for x being Element of Permutations n holds G0 . {x} = (Path_product (0. (K,n,n))) . x
proof
let x be Element of Permutations n; ::_thesis: G0 . {x} = (Path_product (0. (K,n,n))) . x
 G0 . {.x.} = 0. K by FUNCOP_1:7;
hence  G0 . {x} = (Path_product (0. (K,n,n))) . x by A19, FUNCOP_1:7; ::_thesis: verum
end;
A21: for B9 being Element of Fin (Permutations n) st B9 c= FinOmega (Permutations n) & B9 <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (0. (K,n,n))) . x))
proof
let B9 be Element of Fin (Permutations n); ::_thesis: ( B9 c= FinOmega (Permutations n) & B9 <> {} implies for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (0. (K,n,n))) . x)) )
assume that
 B9 c= FinOmega (Permutations n) and
 B9 <> {} ; ::_thesis: for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (0. (K,n,n))) . x))
thus  for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (0. (K,n,n))) . x)) ::_thesis: verum
proof
let x be Element of Permutations n; ::_thesis: ( x in (FinOmega (Permutations n)) \ B9 implies G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (0. (K,n,n))) . x)) )
assume  x in (FinOmega (Permutations n)) \ B9 ; ::_thesis: G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (0. (K,n,n))) . x))
A22: ( G0 . (B9 \/ {.x.}) = 0. K & G0 . B9 = 0. K ) by FUNCOP_1:7;
 ( (Path_product (0. (K,n,n))) . x = 0. K & 0. K is_a_unity_wrt the addF of K ) by A19, FUNCOP_1:7, FVSUM_1:6;
hence  G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (0. (K,n,n))) . x)) by A22, BINOP_1:3; ::_thesis: verum
end;
end;
 ( FinOmega (Permutations n) <> {} or the addF of K is having_a_unity ) by MATRIX_2:26, MATRIX_2:def_14;
then  the addF of K $$ ((FinOmega (Permutations n)),(Path_product (0. (K,n,n)))) = 0. K by A1, A2, A20, A21, SETWISEO:def_3;
hence  Det (0. (K,n,n)) = 0. K by MATRIX_3:def_9; ::_thesis: verum
end;

definition
let x, y, a, b be set ;
func IFIN (x,y,a,b) ->  set  equals :Def1: :: MATRIX_7:def 1
a if x in y
otherwise b;
correctness
coherence
( ( x in y implies a is set ) & ( not x in y implies b is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def1 defines IFIN MATRIX_7:def_1_:_
 for x, y, a, b being set holds
( ( x in y implies IFIN (x,y,a,b) = a ) & ( not x in y implies IFIN (x,y,a,b) = b ) );

theorem :: MATRIX_7:16
for K being Field
for n being Element of NAT st n >= 1 holds
Det (1. (K,n)) = 1_ K
proof
let K be Field; ::_thesis: for n being Element of NAT st n >= 1 holds
Det (1. (K,n)) = 1_ K
let n be Element of NAT ; ::_thesis: ( n >= 1 implies Det (1. (K,n)) = 1_ K )
assume A1: n >= 1 ; ::_thesis: Det (1. (K,n)) = 1_ K
deffunc H1( set ) ->  Element of the carrier of K = IFEQ ((idseq n),$1,(1_ K),(0. K));
set X = Permutations n;
set Y = the carrier of K;
A2: for x being set st x in Permutations n holds
H1(x) in the carrier of K ;
 ex f2 being Function of (Permutations n), the carrier of K st
for x being set st x in Permutations n holds
f2 . x = H1(x) from FUNCT_2:sch_2(A2);
then consider f2 being Function of (Permutations n), the carrier of K such that
A3: for x being set st x in Permutations n holds
f2 . x = H1(x) ;
A4: id (Seg n) is even by MATRIX_2:25;
A5: for x being set st x in dom (Path_product (1. (K,n))) holds
(Path_product (1. (K,n))) . x = f2 . x
proof
let x be set ; ::_thesis: ( x in dom (Path_product (1. (K,n))) implies (Path_product (1. (K,n))) . x = f2 . x )
assume  x in dom (Path_product (1. (K,n))) ; ::_thesis: (Path_product (1. (K,n))) . x = f2 . x
 for p being Element of Permutations n holds f2 . p = - (( the multF of K $$ (Path_matrix (p,(1. (K,n))))),p)
proof
defpred S1[ Element of NAT ] means  the multF of K $$ (($1 + 1) |-> (1_ K)) = 1_ K;
let p be Element of Permutations n; ::_thesis: f2 . p = - (( the multF of K $$ (Path_matrix (p,(1. (K,n))))),p)
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A7: ((k + 1) + 1) |-> (1_ K) = ((k + 1) |-> (1_ K)) ^ <*(1_ K)*> by FINSEQ_2:60;
assume  S1[k] ; ::_thesis: S1[k + 1]
then  the multF of K $$ (((k + 1) + 1) |-> (1_ K)) = (1_ K) * (1_ K) by A7, FINSOP_1:4
.= 1_ K by GROUP_1:def_4 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
A8: now__::_thesis:_(_(_p_is_even_&_-_((0._K),p)_=_0._K_)_or_(_not_p_is_even_&_-_((0._K),p)_=_0._K_)_)
percases ( p is even or not p is even ) ;
case p is even ; ::_thesis: - ((0. K),p) = 0. K
hence  - ((0. K),p) = 0. K by MATRIX_2:def_13; ::_thesis: verum
end;
case not p is even ; ::_thesis: - ((0. K),p) = 0. K
then  - ((0. K),p) = - (0. K) by MATRIX_2:def_13
.= 0. K by RLVECT_1:12 ;
hence  - ((0. K),p) = 0. K ; ::_thesis: verum
end;
end;
end;
 n -' 1 = n - 1 by A1, XREAL_1:233;
then A9: (n -' 1) + 1 = n ;
 1 |-> (1_ K) = <*(1_ K)*> by FINSEQ_2:59;
then A10: S1[ 0 ] by FINSOP_1:11;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A10, A6);
then A11: ( len (n |-> (1_ K)) = n & the multF of K $$ (n |-> (1_ K)) = 1_ K ) by A9, CARD_1:def_7;
now__::_thesis:_(_(_p_=_idseq_n_&_f2_._p_=_-_((_the_multF_of_K_$$_(Path_matrix_(p,(1._(K,n))))),p)_)_or_(_p_<>_idseq_n_&_f2_._p_=_-_((_the_multF_of_K_$$_(Path_matrix_(p,(1._(K,n))))),p)_)_)
percases ( p = idseq n or p <> idseq n ) ;
caseA12: p = idseq n ; ::_thesis: f2 . p = - (( the multF of K $$ (Path_matrix (p,(1. (K,n))))),p)
A13: for i, j being Nat st i in dom (n |-> (1_ K)) & j = p . i holds
(n |-> (1_ K)) . i = (1. (K,n)) * (i,j)
proof
A14: Indices (1. (K,n)) = [:(Seg n),(Seg n):] by A1, MATRIX_1:23;
let i, j be Nat; ::_thesis: ( i in dom (n |-> (1_ K)) & j = p . i implies (n |-> (1_ K)) . i = (1. (K,n)) * (i,j) )
assume that
A15: i in dom (n |-> (1_ K)) and
A16: j = p . i ; ::_thesis: (n |-> (1_ K)) . i = (1. (K,n)) * (i,j)
A17: i in Seg n by A15, FUNCOP_1:13;
then  j in Seg n by A16, Th14;
then A18: [i,j] in Indices (1. (K,n)) by A17, A14, ZFMISC_1:def_2;
 ( (n |-> (1_ K)) . i = 1_ K & p . i = i ) by A12, A17, FUNCOP_1:7, FUNCT_1:17;
hence  (n |-> (1_ K)) . i = (1. (K,n)) * (i,j) by A16, A18, MATRIX_1:def_11; ::_thesis: verum
end;
 len (Permutations n) = n by MATRIX_2:18;
then A19: - (( the multF of K $$ (Path_matrix (p,(1. (K,n))))),p) = the multF of K $$ (Path_matrix (p,(1. (K,n)))) by A4, A12, MATRIX_2:def_13;
f2 . p = H1(p) by A3
.= 1_ K by A12, FUNCOP_1:def_8 ;
hence  f2 . p = - (( the multF of K $$ (Path_matrix (p,(1. (K,n))))),p) by A11, A19, A13, MATRIX_3:def_7; ::_thesis: verum
end;
caseA20: p <> idseq n ; ::_thesis: f2 . p = - (( the multF of K $$ (Path_matrix (p,(1. (K,n))))),p)
reconsider A = NAT as non empty set ;
defpred S2[ Element of NAT ] means ( $1 < n implies ex p3 being FinSequence of K st
( len p3 = $1 + 1 & p3 . 1 = (Path_matrix (p,(1. (K,n)))) . 1 & ( for n3 being Element of NAT st 0 <> n3 & n3 < $1 + 1 & n3 < n holds
p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1))) ) ) );
A21: rng (Path_matrix (p,(1. (K,n)))) c= the carrier of K by FINSEQ_1:def_4;
A22: len (Path_matrix (p,(1. (K,n)))) = n by MATRIX_3:def_7;
then  1 in Seg (len (Path_matrix (p,(1. (K,n))))) by A1;
then  1 in dom (Path_matrix (p,(1. (K,n)))) by FINSEQ_1:def_3;
then  (Path_matrix (p,(1. (K,n)))) . 1 in rng (Path_matrix (p,(1. (K,n)))) by FUNCT_1:def_3;
then reconsider d = (Path_matrix (p,(1. (K,n)))) . 1 as Element of K by A21;
reconsider q3 = <*d*> as FinSequence of K ;
A23: for n3 being Element of NAT st 0 <> n3 & n3 < 0 + 1 & n3 < n holds
q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1))) by NAT_1:13;
A24: dom p = Seg (len (Permutations n)) by FUNCT_2:52;
then A25: dom p = Seg n by MATRIX_2:18;
then  dom p = dom (idseq n) by RELAT_1:45;
then consider i0 being set  such that
A26: i0 in dom p and
A27: p . i0 <> (idseq n) . i0 by A20, FUNCT_1:2;
reconsider i0 = i0 as Element of NAT by A24, A26;
A28: p . i0 <> i0 by A25, A26, A27, FUNCT_1:18;
A29: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A30: S2[k] ; ::_thesis: S2[k + 1]
now__::_thesis:_(_(_k_+_1_<_n_&_S2[k_+_1]_)_or_(_k_+_1_>=_n_&_S2[k_+_1]_)_)
percases ( k + 1 < n or k + 1 >= n ) ;
caseA31: k + 1 < n ; ::_thesis: S2[k + 1]
then consider p3 being FinSequence of K such that
A32: len p3 = k + 1 and
A33: p3 . 1 = (Path_matrix (p,(1. (K,n)))) . 1 and
A34: for n3 being Element of NAT st 0 <> n3 & n3 < k + 1 & n3 < n holds
p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1))) by A30, NAT_1:12;
defpred S3[ set , set ] means ( ( $1 in Seg (k + 1) implies $2 = p3 . $1 ) & ( not $1 in Seg (k + 1) implies $2 = 0. K ) );
A35: for x being set st x in NAT holds
ex y being set st
( y in the carrier of K & S3[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in the carrier of K & S3[x,y] ) )
assume  x in NAT ; ::_thesis: ex y being set st
( y in the carrier of K & S3[x,y] )
now__::_thesis:_(_(_x_in_Seg_(k_+_1)_&_ex_y_being_set_st_
(_y_in_the_carrier_of_K_&_S3[x,y]_)_)_or_(_not_x_in_Seg_(k_+_1)_&_ex_y_being_set_st_
(_y_in_the_carrier_of_K_&_S3[x,y]_)_)_)
percases ( x in Seg (k + 1) or not x in Seg (k + 1) ) ;
caseA36: x in Seg (k + 1) ; ::_thesis: ex y being set st
( y in the carrier of K & S3[x,y] )
then reconsider nx = x as Element of NAT ;
 nx in dom p3 by A32, A36, FINSEQ_1:def_3;
then A37: p3 . nx in rng p3 by FUNCT_1:def_3;
 rng p3 c= the carrier of K by FINSEQ_1:def_4;
then reconsider s = p3 . nx as Element of K by A37;
 ( x in Seg (k + 1) implies s = p3 . x ) ;
hence  ex y being set st
( y in the carrier of K & S3[x,y] ) by A36; ::_thesis: verum
end;
case not x in Seg (k + 1) ; ::_thesis: ex y being set st
( y in the carrier of K & S3[x,y] )
hence  ex y being set st
( y in the carrier of K & S3[x,y] ) ; ::_thesis: verum
end;
end;
end;
hence  ex y being set st
( y in the carrier of K & S3[x,y] ) ; ::_thesis: verum
end;
 ex f6 being Function of NAT, the carrier of K st
for x being set st x in NAT holds
S3[x,f6 . x] from FUNCT_2:sch_1(A35);
then consider f6 being Function of NAT, the carrier of K such that
A38: for x being set st x in NAT holds
S3[x,f6 . x] ;
 ( 1 <= (k + 1) + 1 & (k + 1) + 1 <= n ) by A31, NAT_1:12, NAT_1:13;
then  (k + 1) + 1 in Seg (len (Path_matrix (p,(1. (K,n))))) by A22;
then  (k + 1) + 1 in dom (Path_matrix (p,(1. (K,n)))) by FINSEQ_1:def_3;
then  ( rng (Path_matrix (p,(1. (K,n)))) c= the carrier of K & (Path_matrix (p,(1. (K,n)))) . ((k + 1) + 1) in rng (Path_matrix (p,(1. (K,n)))) ) by FINSEQ_1:def_4, FUNCT_1:def_3;
then  [(f6 . (k + 1)),((Path_matrix (p,(1. (K,n)))) . ((k + 1) + 1))] in [: the carrier of K, the carrier of K:] by ZFMISC_1:def_2;
then reconsider e = the multF of K . ((f6 . (k + 1)),((Path_matrix (p,(1. (K,n)))) . ((k + 1) + 1))) as Element of K by FUNCT_2:5;
reconsider q3 = p3 ^ <*e*> as FinSequence of K ;
A39: len q3 = (len p3) + (len <*e*>) by FINSEQ_1:22
.= (k + 1) + 1 by A32, FINSEQ_1:40 ;
A40: for n3 being Element of NAT st 0 <> n3 & n3 < (k + 1) + 1 & n3 < n holds
q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1)))
proof
let n3 be Element of NAT ; ::_thesis: ( 0 <> n3 & n3 < (k + 1) + 1 & n3 < n implies q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1))) )
assume that
A41: 0 <> n3 and
A42: n3 < (k + 1) + 1 and
A43: n3 < n ; ::_thesis: q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1)))
now__::_thesis:_(_(_n3_<_k_+_1_&_q3_._(n3_+_1)_=_the_multF_of_K_._((q3_._n3),((Path_matrix_(p,(1._(K,n))))_._(n3_+_1)))_)_or_(_n3_>=_k_+_1_&_q3_._(n3_+_1)_=_the_multF_of_K_._((q3_._n3),((Path_matrix_(p,(1._(K,n))))_._(n3_+_1)))_)_)
percases ( n3 < k + 1 or n3 >= k + 1 ) ;
caseA44: n3 < k + 1 ; ::_thesis: q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1)))
then  ( 1 <= n3 + 1 & n3 + 1 <= k + 1 ) by NAT_1:12, NAT_1:13;
then  n3 + 1 in Seg (len p3) by A32;
then  n3 + 1 in dom p3 by FINSEQ_1:def_3;
then A45: p3 . (n3 + 1) = q3 . (n3 + 1) by FINSEQ_1:def_7;
 0 + 1 <= n3 by A41, NAT_1:13;
then  n3 in Seg (len p3) by A32, A44;
then A46: n3 in dom p3 by FINSEQ_1:def_3;
 p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1))) by A34, A41, A43, A44;
hence  q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1))) by A45, A46, FINSEQ_1:def_7; ::_thesis: verum
end;
caseA47: n3 >= k + 1 ; ::_thesis: q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1)))
A48: n3 + 1 <= (k + 1) + 1 by A42, NAT_1:13;
A49: n3 + 1 > k + 1 by A47, NAT_1:13;
then  n3 + 1 >= (k + 1) + 1 by NAT_1:13;
then A50: n3 + 1 = (k + 1) + 1 by A48, XXREAL_0:1;
 1 <= k + 1 by NAT_1:12;
then A51: k + 1 in Seg (k + 1) ;
then  k + 1 in dom p3 by A32, FINSEQ_1:def_3;
then A52: q3 . (k + 1) = p3 . (k + 1) by FINSEQ_1:def_7;
q3 . (n3 + 1) = <*e*> . ((n3 + 1) - (k + 1)) by A32, A39, A49, A48, FINSEQ_1:24
.= e by A50, FINSEQ_1:def_8 ;
hence  q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1))) by A38, A50, A51, A52; ::_thesis: verum
end;
end;
end;
hence  q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1))) ; ::_thesis: verum
end;
 1 <= k + 1 by NAT_1:12;
then  1 in Seg (len p3) by A32;
then  1 in dom p3 by FINSEQ_1:def_3;
then  q3 . 1 = (Path_matrix (p,(1. (K,n)))) . 1 by A33, FINSEQ_1:def_7;
hence  S2[k + 1] by A39, A40; ::_thesis: verum
end;
case k + 1 >= n ; ::_thesis: S2[k + 1]
hence  S2[k + 1] ; ::_thesis: verum
end;
end;
end;
hence  S2[k + 1] ; ::_thesis: verum
end;
 n < n + 1 by NAT_1:13;
then A53: n - 1 < (n + 1) - 1 by XREAL_1:14;
A54: f2 . p = H1(p) by A3
.= 0. K by A20, FUNCOP_1:def_8 ;
A55: n - 1 = n -' 1 by A1, XREAL_1:233;
 ( len q3 = 1 & q3 . 1 = (Path_matrix (p,(1. (K,n)))) . 1 ) by FINSEQ_1:40;
then A56: S2[ 0 ] by A23;
 for k being Element of NAT holds S2[k] from NAT_1:sch_1(A56, A29);
then consider p3 being FinSequence of K such that
A57: len p3 = (n -' 1) + 1 and
A58: p3 . 1 = (Path_matrix (p,(1. (K,n)))) . 1 and
A59: for n3 being Element of NAT st 0 <> n3 & n3 < (n -' 1) + 1 & n3 < n holds
p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1))) by A55, A53;
defpred S3[ set , set ] means ( ( $1 in Seg n implies $2 = p3 . $1 ) & ( not $1 in Seg n implies $2 = 0. K ) );
A60: for x3 being Element of A ex y3 being Element of K st S3[x3,y3]
proof
let x3 be Element of A; ::_thesis: ex y3 being Element of K st S3[x3,y3]
now__::_thesis:_(_(_x3_in_Seg_n_&_ex_y3_being_Element_of_K_st_S3[x3,y3]_)_or_(_not_x3_in_Seg_n_&_ex_y3_being_Element_of_K_st_S3[x3,y3]_)_)
percases ( x3 in Seg n or not x3 in Seg n ) ;
caseA61: x3 in Seg n ; ::_thesis: ex y3 being Element of K st S3[x3,y3]
then  x3 in dom p3 by A55, A57, FINSEQ_1:def_3;
then  ( rng p3 c= the carrier of K & p3 . x3 in rng p3 ) by FINSEQ_1:def_4, FUNCT_1:def_3;
hence  ex y3 being Element of K st S3[x3,y3] by A61; ::_thesis: verum
end;
case not x3 in Seg n ; ::_thesis: ex y3 being Element of K st S3[x3,y3]
hence  ex y3 being Element of K st S3[x3,y3] ; ::_thesis: verum
end;
end;
end;
hence  ex y3 being Element of K st S3[x3,y3] ; ::_thesis: verum
end;
 ex f4 being Function of A, the carrier of K st
for x2 being Element of A holds S3[x2,f4 . x2] from FUNCT_2:sch_3(A60);
then consider f4 being Function of NAT, the carrier of K such that
A62: for x4 being Element of NAT holds
( ( x4 in Seg n implies f4 . x4 = p3 . x4 ) & ( not x4 in Seg n implies f4 . x4 = 0. K ) ) ;
 p is Permutation of (Seg n) by MATRIX_2:def_9;
then A63: p . i0 in Seg n by A25, A26, FUNCT_2:5;
then reconsider j0 = p . i0 as Element of NAT ;
 Indices (1. (K,n)) = [:(Seg n),(Seg n):] by A1, MATRIX_1:23;
then A64: [i0,j0] in Indices (1. (K,n)) by A25, A26, A63, ZFMISC_1:def_2;
 i0 <= n by A25, A26, FINSEQ_1:1;
then A65: n -' i0 = n - i0 by XREAL_1:233;
 i0 in dom (Path_matrix (p,(1. (K,n)))) by A25, A26, A22, FINSEQ_1:def_3;
then A66: (Path_matrix (p,(1. (K,n)))) . i0 = (1. (K,n)) * (i0,j0) by MATRIX_3:def_7;
defpred S4[ Element of NAT ] means f4 . (i0 + $1) = 0. K;
A67: 0 < i0 by A24, A26, FINSEQ_1:1;
A68: for k being Element of NAT st S4[k] holds
S4[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S4[k] implies S4[k + 1] )
A69: 1 <= 1 + (i0 + k) by NAT_1:12;
assume A70: S4[k] ; ::_thesis: S4[k + 1]
now__::_thesis:_(_(_(i0_+_k)_+_1_<=_n_&_S4[k_+_1]_)_or_(_(i0_+_k)_+_1_>_n_&_S4[k_+_1]_)_)
percases ( (i0 + k) + 1 <= n or (i0 + k) + 1 > n ) ;
caseA71: (i0 + k) + 1 <= n ; ::_thesis: S4[k + 1]
 1 <= 1 + (i0 + k) by NAT_1:12;
then  (i0 + k) + 1 in Seg (len (Path_matrix (p,(1. (K,n))))) by A22, A71;
then  (i0 + k) + 1 in dom (Path_matrix (p,(1. (K,n)))) by FINSEQ_1:def_3;
then A72: (Path_matrix (p,(1. (K,n)))) . ((i0 + k) + 1) in rng (Path_matrix (p,(1. (K,n)))) by FUNCT_1:def_3;
 rng (Path_matrix (p,(1. (K,n)))) c= the carrier of K by FINSEQ_1:def_4;
then reconsider b = (Path_matrix (p,(1. (K,n)))) . ((i0 + k) + 1) as Element of K by A72;
A73: i0 + k < n by A71, NAT_1:13;
 0 + 1 <= i0 + k by A67, NAT_1:13;
then A74: i0 + k in Seg n by A73;
 (i0 + k) + 1 in Seg n by A69, A71;
then f4 . ((i0 + k) + 1) = p3 . ((i0 + k) + 1) by A62
.= the multF of K . ((p3 . (i0 + k)),((Path_matrix (p,(1. (K,n)))) . ((i0 + k) + 1))) by A55, A59, A67, A73
.= (0. K) * b by A62, A70, A74
.= 0. K by VECTSP_1:6 ;
hence  S4[k + 1] ; ::_thesis: verum
end;
case (i0 + k) + 1 > n ; ::_thesis: S4[k + 1]
then  not i0 + (k + 1) in Seg n by FINSEQ_1:1;
hence  S4[k + 1] by A62; ::_thesis: verum
end;
end;
end;
hence  S4[k + 1] ; ::_thesis: verum
end;
 1 in Seg n by A1;
then A75: f4 . 1 = (Path_matrix (p,(1. (K,n)))) . 1 by A58, A62;
A76: for n3 being Element of NAT st 0 <> n3 & n3 < len (Path_matrix (p,(1. (K,n)))) holds
f4 . (n3 + 1) = the multF of K . ((f4 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1)))
proof
let n3 be Element of NAT ; ::_thesis: ( 0 <> n3 & n3 < len (Path_matrix (p,(1. (K,n)))) implies f4 . (n3 + 1) = the multF of K . ((f4 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1))) )
assume that
A77: 0 <> n3 and
A78: n3 < len (Path_matrix (p,(1. (K,n)))) ; ::_thesis: f4 . (n3 + 1) = the multF of K . ((f4 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1)))
A79: n3 + 1 <= len (Path_matrix (p,(1. (K,n)))) by A78, NAT_1:13;
A80: 0 + 1 <= n3 by A77, NAT_1:13;
then A81: n3 in Seg n by A22, A78;
 1 < n3 + 1 by A80, NAT_1:13;
then  n3 + 1 in Seg n by A22, A79;
then A82: f4 . (n3 + 1) = p3 . (n3 + 1) by A62;
 p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1))) by A22, A55, A59, A77, A78;
hence  f4 . (n3 + 1) = the multF of K . ((f4 . n3),((Path_matrix (p,(1. (K,n)))) . (n3 + 1))) by A62, A82, A81; ::_thesis: verum
end;
A83: 1 <= i0 by A24, A26, FINSEQ_1:1;
now__::_thesis:_(_(_i0_<=_1_&_S4[_0_]_)_or_(_i0_>_1_&_S4[_0_]_)_)
percases ( i0 <= 1 or i0 > 1 ) ;
case i0 <= 1 ; ::_thesis: S4[ 0 ]
then  i0 = 1 by A83, XXREAL_0:1;
hence  S4[ 0 ] by A28, A66, A64, A75, MATRIX_1:def_11; ::_thesis: verum
end;
caseA84: i0 > 1 ; ::_thesis: S4[ 0 ]
reconsider a = f4 . (i0 -' 1) as Element of K ;
 i0 < i0 + 1 by NAT_1:13;
then A85: i0 - 1 < (i0 + 1) - 1 by XREAL_1:14;
 i0 <= n by A25, A26, FINSEQ_1:1;
then A86: i0 - 1 < len (Path_matrix (p,(1. (K,n)))) by A22, A85, XXREAL_0:2;
 i0 -' 1 = i0 - 1 by A84, XREAL_1:233;
then A87: (i0 -' 1) + 1 = i0 ;
 i0 - 1 > 1 - 1 by A84, XREAL_1:14;
then f4 . i0 = the multF of K . ((f4 . (i0 -' 1)),((Path_matrix (p,(1. (K,n)))) . i0)) by A76, A86, A87
.= a * (0. K) by A28, A66, A64, MATRIX_1:def_11
.= 0. K by VECTSP_1:6 ;
hence  S4[ 0 ] ; ::_thesis: verum
end;
end;
end;
then A88: S4[ 0 ] ;
 for k being Element of NAT holds S4[k] from NAT_1:sch_1(A88, A68);
then  S4[n -' i0] ;
hence  f2 . p = - (( the multF of K $$ (Path_matrix (p,(1. (K,n))))),p) by A1, A8, A54, A22, A75, A76, A65, FINSOP_1:2; ::_thesis: verum
end;
end;
end;
hence  f2 . p = - (( the multF of K $$ (Path_matrix (p,(1. (K,n))))),p) ; ::_thesis: verum
end;
hence  (Path_product (1. (K,n))) . x = f2 . x by MATRIX_3:def_8; ::_thesis: verum
end;
deffunc H2( set ) ->  set = IFIN ((idseq n),$1,(1_ K),(0. K));
set F = the addF of K;
set f = Path_product (1. (K,n));
set B = FinOmega (Permutations n);
A89: for x being set st x in Fin (Permutations n) holds
H2(x) in the carrier of K
proof
let x be set ; ::_thesis: ( x in Fin (Permutations n) implies H2(x) in the carrier of K )
assume  x in Fin (Permutations n) ; ::_thesis: H2(x) in the carrier of K
now__::_thesis:_(_(_idseq_n_in_x_&_H2(x)_in_the_carrier_of_K_)_or_(_not_idseq_n_in_x_&_H2(x)_in_the_carrier_of_K_)_)
percases ( idseq n in x or not idseq n in x ) ;
case idseq n in x ; ::_thesis: H2(x) in the carrier of K
then  H2(x) = 1_ K by Def1;
hence  H2(x) in the carrier of K ; ::_thesis: verum
end;
case not idseq n in x ; ::_thesis: H2(x) in the carrier of K
then  H2(x) = 0. K by Def1;
hence  H2(x) in the carrier of K ; ::_thesis: verum
end;
end;
end;
hence  H2(x) in the carrier of K ; ::_thesis: verum
end;
 ex f2 being Function of (Fin (Permutations n)), the carrier of K st
for x being set st x in Fin (Permutations n) holds
f2 . x = H2(x) from FUNCT_2:sch_2(A89);
then consider G0 being Function of (Fin (Permutations n)), the carrier of K such that
A90: for x being set st x in Fin (Permutations n) holds
G0 . x = H2(x) ;
 dom f2 = Permutations n by FUNCT_2:def_1;
then A91: dom (Path_product (1. (K,n))) = dom f2 by FUNCT_2:def_1;
then A92: Path_product (1. (K,n)) = f2 by A5, FUNCT_1:2;
A93: for B9 being Element of Fin (Permutations n) st B9 c= FinOmega (Permutations n) & B9 <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x))
proof
let B9 be Element of Fin (Permutations n); ::_thesis: ( B9 c= FinOmega (Permutations n) & B9 <> {} implies for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) )
assume that
 B9 c= FinOmega (Permutations n) and
 B9 <> {} ; ::_thesis: for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x))
thus  for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) ::_thesis: verum
proof
let x be Element of Permutations n; ::_thesis: ( x in (FinOmega (Permutations n)) \ B9 implies G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) )
assume A94: x in (FinOmega (Permutations n)) \ B9 ; ::_thesis: G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x))
A95: now__::_thesis:_(_not_idseq_n_in_B9_\/_{x}_implies_G0_._(B9_\/_{x})_=_0._K_)
assume A96: not idseq n in B9 \/ {x} ; ::_thesis: G0 . (B9 \/ {x}) = 0. K
thus G0 . (B9 \/ {x}) = IFIN ((idseq n),(B9 \/ {.x.}),(1_ K),(0. K)) by A90
.= 0. K by A96, Def1 ; ::_thesis: verum
end;
A97: 0. K is_a_unity_wrt the addF of K by FVSUM_1:6;
A98: now__::_thesis:_(_not_idseq_n_in_B9_implies_G0_._B9_=_0._K_)
assume A99: not idseq n in B9 ; ::_thesis: G0 . B9 = 0. K
thus G0 . B9 = IFIN ((idseq n),B9,(1_ K),(0. K)) by A90
.= 0. K by A99, Def1 ; ::_thesis: verum
end;
A100: now__::_thesis:_(_not_idseq_n_in_B9_\/_{x}_implies_the_addF_of_K_._((G0_._B9),((Path_product_(1._(K,n)))_._x))_=_0._K_)
assume A101: not idseq n in B9 \/ {x} ; ::_thesis: the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) = 0. K
then  not idseq n in {x} by XBOOLE_0:def_3;
then A102: not idseq n = x by TARSKI:def_1;
(Path_product (1. (K,n))) . x = H1(x) by A3, A92
.= 0. K by A102, FUNCOP_1:def_8 ;
hence  the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) = 0. K by A98, A97, A101, BINOP_1:3, XBOOLE_0:def_3; ::_thesis: verum
end;
A103: now__::_thesis:_(_idseq_n_in_B9_implies_G0_._B9_=_1__K_)
assume A104: idseq n in B9 ; ::_thesis: G0 . B9 = 1_ K
thus G0 . B9 = IFIN ((idseq n),B9,(1_ K),(0. K)) by A90
.= 1_ K by A104, Def1 ; ::_thesis: verum
end;
A105: now__::_thesis:_(_idseq_n_in_B9_\/_{x}_implies_the_addF_of_K_._((G0_._B9),((Path_product_(1._(K,n)))_._x))_=_1__K_)
assume  idseq n in B9 \/ {x} ; ::_thesis: the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) = 1_ K
then A106: ( idseq n in B9 or idseq n in {x} ) by XBOOLE_0:def_3;
now__::_thesis:_(_(_idseq_n_in_B9_&_the_addF_of_K_._((G0_._B9),((Path_product_(1._(K,n)))_._x))_=_1__K_)_or_(_idseq_n_=_x_&_the_addF_of_K_._((G0_._B9),((Path_product_(1._(K,n)))_._x))_=_1__K_)_)
percases ( idseq n in B9 or idseq n = x ) by A106, TARSKI:def_1;
caseA107: idseq n in B9 ; ::_thesis: the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) = 1_ K
A108: not x in B9 by A94, XBOOLE_0:def_5;
(Path_product (1. (K,n))) . x = H1(x) by A3, A92
.= 0. K by A107, A108, FUNCOP_1:def_8 ;
hence  the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) = 1_ K by A103, A97, A107, BINOP_1:3; ::_thesis: verum
end;
caseA109: idseq n = x ; ::_thesis: the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) = 1_ K
(Path_product (1. (K,n))) . x = H1(x) by A3, A92
.= 1_ K by A109, FUNCOP_1:def_8 ;
hence  the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) = 1_ K by A94, A98, A97, A109, BINOP_1:3, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
hence  the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) = 1_ K ; ::_thesis: verum
end;
now__::_thesis:_(_idseq_n_in_B9_\/_{x}_implies_G0_._(B9_\/_{x})_=_1__K_)
assume A110: idseq n in B9 \/ {x} ; ::_thesis: G0 . (B9 \/ {x}) = 1_ K
thus G0 . (B9 \/ {x}) = IFIN ((idseq n),(B9 \/ {.x.}),(1_ K),(0. K)) by A90
.= 1_ K by A110, Def1 ; ::_thesis: verum
end;
hence  G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) by A95, A105, A100; ::_thesis: verum
end;
end;
A111: for x being Element of Permutations n holds G0 . {x} = (Path_product (1. (K,n))) . x
proof
let x be Element of Permutations n; ::_thesis: G0 . {x} = (Path_product (1. (K,n))) . x
now__::_thesis:_(_(_x_=_idseq_n_&_G0_._{.x.}_=_f2_._x_)_or_(_x_<>_idseq_n_&_G0_._{.x.}_=_f2_._x_)_)
percases ( x = idseq n or x <> idseq n ) ;
caseA112: x = idseq n ; ::_thesis: G0 . {.x.} = f2 . x
then  idseq n in {x} by TARSKI:def_1;
then A113: IFIN ((idseq n),{x},(1_ K),(0. K)) = 1_ K by Def1;
f2 . x = H1(x) by A3
.= 1_ K by A112, FUNCOP_1:def_8 ;
hence  G0 . {.x.} = f2 . x by A90, A113; ::_thesis: verum
end;
caseA114: x <> idseq n ; ::_thesis: G0 . {.x.} = f2 . x
then  not idseq n in {x} by TARSKI:def_1;
then A115: IFIN ((idseq n),{x},(1_ K),(0. K)) = 0. K by Def1;
f2 . x = H1(x) by A3
.= 0. K by A114, FUNCOP_1:def_8 ;
hence  G0 . {.x.} = f2 . x by A90, A115; ::_thesis: verum
end;
end;
end;
hence  G0 . {x} = (Path_product (1. (K,n))) . x by A91, A5, FUNCT_1:2; ::_thesis: verum
end;
A116: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G0 . {} = e
proof
let e be Element of the carrier of K; ::_thesis: ( e is_a_unity_wrt the addF of K implies G0 . {} = e )
assume  e is_a_unity_wrt the addF of K ; ::_thesis: G0 . {} = e
then A117: the addF of K . ((0. K),e) = 0. K by BINOP_1:3;
 0. K is_a_unity_wrt the addF of K by FVSUM_1:6;
then A118: the addF of K . ((0. K),e) = e by BINOP_1:3;
 IFIN ((idseq n),{},(1_ K),(0. K)) = 0. K by Def1;
hence  G0 . {} = e by A90, A117, A118, FINSUB_1:7; ::_thesis: verum
end;
A119: now__::_thesis:_(_idseq_n_in_FinOmega_(Permutations_n)_implies_G0_._(FinOmega_(Permutations_n))_=_1__K_)
assume A120: idseq n in FinOmega (Permutations n) ; ::_thesis: G0 . (FinOmega (Permutations n)) = 1_ K
thus G0 . (FinOmega (Permutations n)) = IFIN ((idseq n),(FinOmega (Permutations n)),(1_ K),(0. K)) by A90
.= 1_ K by A120, Def1 ; ::_thesis: verum
end;
 idseq n is Element of (Group_of_Perm n) by MATRIX_2:20;
then  ( FinOmega (Permutations n) = Permutations n & idseq n in the carrier of (Group_of_Perm n) ) by MATRIX_2:26, MATRIX_2:def_14;
then  the addF of K $$ ((FinOmega (Permutations n)),(Path_product (1. (K,n)))) = 1_ K by A119, A116, A111, A93, MATRIX_2:def_10, SETWISEO:def_3;
hence  Det (1. (K,n)) = 1_ K by MATRIX_3:def_9; ::_thesis: verum
end;

definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
:: original: diagonal
redefine attrM is diagonal  means :Def2: :: MATRIX_7:def 2
 for i, j being Element of NAT st i in Seg n & j in Seg n & i <> j holds
M * (i,j) = 0. K;
compatibility
 ( M is diagonal iff for i, j being Element of NAT st i in Seg n & j in Seg n & i <> j holds
M * (i,j) = 0. K )
proof
hereby  ::_thesis: ( ( for i, j being Element of NAT st i in Seg n & j in Seg n & i <> j holds
M * (i,j) = 0. K ) implies M is diagonal )
assume A1: M is diagonal ; ::_thesis: for i, j being Element of NAT st i in Seg n & j in Seg n & i <> j holds
M * (i,j) = 0. K
let i, j be Element of NAT ; ::_thesis: ( i in Seg n & j in Seg n & i <> j implies M * (i,j) = 0. K )
assume that
A2: ( i in Seg n & j in Seg n ) and
A3: i <> j ; ::_thesis: M * (i,j) = 0. K
 [i,j] in [:(Seg n),(Seg n):] by A2, ZFMISC_1:def_2;
then  [i,j] in Indices M by MATRIX_1:24;
hence  M * (i,j) = 0. K by A1, A3, MATRIX_1:def_14; ::_thesis: verum
end;
assume A4: for i, j being Element of NAT st i in Seg n & j in Seg n & i <> j holds
M * (i,j) = 0. K ; ::_thesis: M is diagonal
let i, j be Nat; :: according to MATRIX_1:def_14 ::_thesis: ( not [i,j] in Indices M or M * (i,j) = 0. K or i = j )
assume that
A5: [i,j] in Indices M and
A6: M * (i,j) <> 0. K ; ::_thesis: i = j
 [i,j] in [:(Seg n),(Seg n):] by A5, MATRIX_1:24;
then  ( i in Seg n & j in Seg n ) by ZFMISC_1:87;
hence  i = j by A4, A6; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines diagonal MATRIX_7:def_2_:_
 for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is diagonal iff for i, j being Element of NAT st i in Seg n & j in Seg n & i <> j holds
M * (i,j) = 0. K );

theorem :: MATRIX_7:17
for K being Field
for n being Element of NAT
for A being Matrix of n,K st n >= 1 & A is V164(b1) holds
Det A = the multF of K $$ (diagonal_of_Matrix A)
proof
let K be Field; ::_thesis: for n being Element of NAT
for A being Matrix of n,K st n >= 1 & A is V164(K) holds
Det A = the multF of K $$ (diagonal_of_Matrix A)
let n be Element of NAT ; ::_thesis: for A being Matrix of n,K st n >= 1 & A is V164(K) holds
Det A = the multF of K $$ (diagonal_of_Matrix A)
let A be Matrix of n,K; ::_thesis: ( n >= 1 & A is V164(K) implies Det A = the multF of K $$ (diagonal_of_Matrix A) )
assume that
A1: n >= 1 and
A2: A is V164(K) ; ::_thesis: Det A = the multF of K $$ (diagonal_of_Matrix A)
set k1 = the multF of K $$ (diagonal_of_Matrix A);
set X = Permutations n;
set Y = the carrier of K;
reconsider p0 = idseq n as Permutation of (Seg n) ;
A3: len (diagonal_of_Matrix A) = n by MATRIX_3:def_10;
deffunc H1( set ) ->  Element of the carrier of K = IFEQ ((idseq n),$1,( the multF of K $$ (diagonal_of_Matrix A)),(0. K));
A4: for x being set st x in Permutations n holds
H1(x) in the carrier of K ;
 ex f2 being Function of (Permutations n), the carrier of K st
for x being set st x in Permutations n holds
f2 . x = H1(x) from FUNCT_2:sch_2(A4);
then consider f2 being Function of (Permutations n), the carrier of K such that
A5: for x being set st x in Permutations n holds
f2 . x = H1(x) ;
A6: p0 is even by MATRIX_2:25;
A7: for x being set st x in dom (Path_product A) holds
(Path_product A) . x = f2 . x
proof
let x be set ; ::_thesis: ( x in dom (Path_product A) implies (Path_product A) . x = f2 . x )
assume  x in dom (Path_product A) ; ::_thesis: (Path_product A) . x = f2 . x
 for p being Element of Permutations n holds f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p)
proof
let p be Element of Permutations n; ::_thesis: f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p)
A8: now__::_thesis:_-_((0._K),p)_=_0._K
percases ( p is even or p is odd ) ;
suppose p is even ; ::_thesis: - ((0. K),p) = 0. K
hence  - ((0. K),p) = 0. K by MATRIX_2:def_13; ::_thesis: verum
end;
suppose p is odd ; ::_thesis: - ((0. K),p) = 0. K
then  - ((0. K),p) = - (0. K) by MATRIX_2:def_13
.= 0. K by RLVECT_1:12 ;
hence  - ((0. K),p) = 0. K ; ::_thesis: verum
end;
end;
end;
now__::_thesis:_(_(_p_=_idseq_n_&_f2_._p_=_-_((_the_multF_of_K_$$_(Path_matrix_(p,A))),p)_)_or_(_p_<>_idseq_n_&_f2_._p_=_-_((_the_multF_of_K_$$_(Path_matrix_(p,A))),p)_)_)
percases ( p = idseq n or p <> idseq n ) ;
caseA9: p = idseq n ; ::_thesis: f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p)
A10: for i, j being Nat st i in dom (diagonal_of_Matrix A) & j = p . i holds
(diagonal_of_Matrix A) . i = A * (i,j)
proof
let i, j be Nat; ::_thesis: ( i in dom (diagonal_of_Matrix A) & j = p . i implies (diagonal_of_Matrix A) . i = A * (i,j) )
assume that
A11: i in dom (diagonal_of_Matrix A) and
A12: j = p . i ; ::_thesis: (diagonal_of_Matrix A) . i = A * (i,j)
A13: i in Seg n by A3, A11, FINSEQ_1:def_3;
then  p . i = i by A9, FUNCT_1:17;
hence  (diagonal_of_Matrix A) . i = A * (i,j) by A12, A13, MATRIX_3:def_10; ::_thesis: verum
end;
 len (Permutations n) = n by MATRIX_2:18;
then A14: - (( the multF of K $$ (Path_matrix (p,A))),p) = the multF of K $$ (Path_matrix (p,A)) by A6, A9, MATRIX_2:def_13;
f2 . p = H1(p) by A5
.= the multF of K $$ (diagonal_of_Matrix A) by A9, FUNCOP_1:def_8 ;
hence  f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p) by A3, A14, A10, MATRIX_3:def_7; ::_thesis: verum
end;
caseA15: p <> idseq n ; ::_thesis: f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p)
reconsider Ab = NAT as non empty set ;
defpred S1[ Element of NAT ] means ( $1 < n implies ex p3 being FinSequence of K st
( len p3 = $1 + 1 & p3 . 1 = (Path_matrix (p,A)) . 1 & ( for n3 being Element of NAT st 0 <> n3 & n3 < $1 + 1 & n3 < n holds
p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,A)) . (n3 + 1))) ) ) );
A16: rng (Path_matrix (p,A)) c= the carrier of K by FINSEQ_1:def_4;
A17: len (Path_matrix (p,A)) = n by MATRIX_3:def_7;
then  1 in Seg (len (Path_matrix (p,A))) by A1;
then  1 in dom (Path_matrix (p,A)) by FINSEQ_1:def_3;
then  (Path_matrix (p,A)) . 1 in rng (Path_matrix (p,A)) by FUNCT_1:def_3;
then reconsider d = (Path_matrix (p,A)) . 1 as Element of K by A16;
reconsider q3 = <*d*> as FinSequence of K ;
A18: for n3 being Element of NAT st 0 <> n3 & n3 < 0 + 1 & n3 < n holds
q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1))) by NAT_1:13;
A19: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A20: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_(_(_k_+_1_<_n_&_S1[k_+_1]_)_or_(_k_+_1_>=_n_&_S1[k_+_1]_)_)
percases ( k + 1 < n or k + 1 >= n ) ;
caseA21: k + 1 < n ; ::_thesis: S1[k + 1]
then consider p3 being FinSequence of K such that
A22: len p3 = k + 1 and
A23: p3 . 1 = (Path_matrix (p,A)) . 1 and
A24: for n3 being Element of NAT st 0 <> n3 & n3 < k + 1 & n3 < n holds
p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,A)) . (n3 + 1))) by A20, NAT_1:12;
defpred S2[ set , set ] means ( ( $1 in Seg (k + 1) implies $2 = p3 . $1 ) & ( not $1 in Seg (k + 1) implies $2 = 0. K ) );
A25: for x being set st x in NAT holds
ex y being set st
( y in the carrier of K & S2[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in the carrier of K & S2[x,y] ) )
assume  x in NAT ; ::_thesis: ex y being set st
( y in the carrier of K & S2[x,y] )
now__::_thesis:_(_(_x_in_Seg_(k_+_1)_&_ex_y_being_set_st_
(_y_in_the_carrier_of_K_&_S2[x,y]_)_)_or_(_not_x_in_Seg_(k_+_1)_&_ex_y_being_set_st_
(_y_in_the_carrier_of_K_&_S2[x,y]_)_)_)
percases ( x in Seg (k + 1) or not x in Seg (k + 1) ) ;
caseA26: x in Seg (k + 1) ; ::_thesis: ex y being set st
( y in the carrier of K & S2[x,y] )
then reconsider nx = x as Element of NAT ;
 nx in dom p3 by A22, A26, FINSEQ_1:def_3;
then A27: p3 . nx in rng p3 by FUNCT_1:def_3;
 rng p3 c= the carrier of K by FINSEQ_1:def_4;
then reconsider s = p3 . nx as Element of K by A27;
 ( x in Seg (k + 1) implies s = p3 . x ) ;
hence  ex y being set st
( y in the carrier of K & S2[x,y] ) by A26; ::_thesis: verum
end;
case not x in Seg (k + 1) ; ::_thesis: ex y being set st
( y in the carrier of K & S2[x,y] )
hence  ex y being set st
( y in the carrier of K & S2[x,y] ) ; ::_thesis: verum
end;
end;
end;
hence  ex y being set st
( y in the carrier of K & S2[x,y] ) ; ::_thesis: verum
end;
 ex f6 being Function of NAT, the carrier of K st
for x being set st x in NAT holds
S2[x,f6 . x] from FUNCT_2:sch_1(A25);
then consider f6 being Function of NAT, the carrier of K such that
A28: for x being set st x in NAT holds
S2[x,f6 . x] ;
 ( 1 <= (k + 1) + 1 & (k + 1) + 1 <= n ) by A21, NAT_1:12, NAT_1:13;
then  (k + 1) + 1 in Seg (len (Path_matrix (p,A))) by A17;
then  (k + 1) + 1 in dom (Path_matrix (p,A)) by FINSEQ_1:def_3;
then  ( rng (Path_matrix (p,A)) c= the carrier of K & (Path_matrix (p,A)) . ((k + 1) + 1) in rng (Path_matrix (p,A)) ) by FINSEQ_1:def_4, FUNCT_1:def_3;
then  [(f6 . (k + 1)),((Path_matrix (p,A)) . ((k + 1) + 1))] in [: the carrier of K, the carrier of K:] by ZFMISC_1:def_2;
then reconsider e = the multF of K . ((f6 . (k + 1)),((Path_matrix (p,A)) . ((k + 1) + 1))) as Element of K by FUNCT_2:5;
reconsider q3 = p3 ^ <*e*> as FinSequence of K ;
A29: len q3 = (len p3) + (len <*e*>) by FINSEQ_1:22
.= (k + 1) + 1 by A22, FINSEQ_1:40 ;
A30: for n3 being Element of NAT st 0 <> n3 & n3 < (k + 1) + 1 & n3 < n holds
q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1)))
proof
let n3 be Element of NAT ; ::_thesis: ( 0 <> n3 & n3 < (k + 1) + 1 & n3 < n implies q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1))) )
assume that
A31: 0 <> n3 and
A32: n3 < (k + 1) + 1 and
A33: n3 < n ; ::_thesis: q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1)))
now__::_thesis:_(_(_n3_<_k_+_1_&_q3_._(n3_+_1)_=_the_multF_of_K_._((q3_._n3),((Path_matrix_(p,A))_._(n3_+_1)))_)_or_(_n3_>=_k_+_1_&_q3_._(n3_+_1)_=_the_multF_of_K_._((q3_._n3),((Path_matrix_(p,A))_._(n3_+_1)))_)_)
percases ( n3 < k + 1 or n3 >= k + 1 ) ;
caseA34: n3 < k + 1 ; ::_thesis: q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1)))
then  ( 1 <= n3 + 1 & n3 + 1 <= k + 1 ) by NAT_1:12, NAT_1:13;
then  n3 + 1 in Seg (len p3) by A22;
then  n3 + 1 in dom p3 by FINSEQ_1:def_3;
then A35: p3 . (n3 + 1) = q3 . (n3 + 1) by FINSEQ_1:def_7;
 0 + 1 <= n3 by A31, NAT_1:13;
then  n3 in Seg (len p3) by A22, A34;
then A36: n3 in dom p3 by FINSEQ_1:def_3;
 p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,A)) . (n3 + 1))) by A24, A31, A33, A34;
hence  q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1))) by A35, A36, FINSEQ_1:def_7; ::_thesis: verum
end;
caseA37: n3 >= k + 1 ; ::_thesis: q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1)))
A38: n3 + 1 <= (k + 1) + 1 by A32, NAT_1:13;
A39: n3 + 1 > k + 1 by A37, NAT_1:13;
then  n3 + 1 >= (k + 1) + 1 by NAT_1:13;
then A40: n3 + 1 = (k + 1) + 1 by A38, XXREAL_0:1;
 1 <= k + 1 by NAT_1:12;
then A41: k + 1 in Seg (k + 1) ;
then  k + 1 in dom p3 by A22, FINSEQ_1:def_3;
then A42: q3 . (k + 1) = p3 . (k + 1) by FINSEQ_1:def_7;
q3 . (n3 + 1) = <*e*> . ((n3 + 1) - (k + 1)) by A22, A29, A39, A38, FINSEQ_1:24
.= e by A40, FINSEQ_1:def_8 ;
hence  q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1))) by A28, A40, A41, A42; ::_thesis: verum
end;
end;
end;
hence  q3 . (n3 + 1) = the multF of K . ((q3 . n3),((Path_matrix (p,A)) . (n3 + 1))) ; ::_thesis: verum
end;
 1 <= k + 1 by NAT_1:12;
then  1 in Seg (len p3) by A22;
then  1 in dom p3 by FINSEQ_1:def_3;
then  q3 . 1 = (Path_matrix (p,A)) . 1 by A23, FINSEQ_1:def_7;
hence  S1[k + 1] by A29, A30; ::_thesis: verum
end;
case k + 1 >= n ; ::_thesis: S1[k + 1]
hence  S1[k + 1] ; ::_thesis: verum
end;
end;
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A43: f2 . p = H1(p) by A5
.= 0. K by A15, FUNCOP_1:def_8 ;
 n < n + 1 by NAT_1:13;
then A44: n - 1 < (n + 1) - 1 by XREAL_1:14;
A45: dom p = Seg (len (Permutations n)) by FUNCT_2:52;
then A46: dom p = Seg n by MATRIX_2:18;
then  dom p = dom (idseq n) by RELAT_1:45;
then consider i0 being set  such that
A47: i0 in dom p and
A48: p . i0 <> (idseq n) . i0 by A15, FUNCT_1:2;
A49: i0 in Seg n by A45, A47, MATRIX_2:18;
reconsider i0 = i0 as Element of NAT by A45, A47;
A50: p . i0 <> i0 by A46, A47, A48, FUNCT_1:18;
 p is Permutation of (Seg n) by MATRIX_2:def_9;
then A51: p . i0 in Seg n by A46, A47, FUNCT_2:5;
then reconsider j0 = p . i0 as Element of NAT ;
A52: n - 1 = n -' 1 by A1, XREAL_1:233;
 ( len q3 = 1 & q3 . 1 = (Path_matrix (p,A)) . 1 ) by FINSEQ_1:40;
then A53: S1[ 0 ] by A18;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A53, A19);
then consider p3 being FinSequence of K such that
A54: len p3 = (n -' 1) + 1 and
A55: p3 . 1 = (Path_matrix (p,A)) . 1 and
A56: for n3 being Element of NAT st 0 <> n3 & n3 < (n -' 1) + 1 & n3 < n holds
p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,A)) . (n3 + 1))) by A52, A44;
defpred S2[ set , set ] means ( ( $1 in Seg n implies $2 = p3 . $1 ) & ( not $1 in Seg n implies $2 = 0. K ) );
A57: for x3 being Element of Ab ex y3 being Element of K st S2[x3,y3]
proof
let x3 be Element of Ab; ::_thesis: ex y3 being Element of K st S2[x3,y3]
now__::_thesis:_(_(_x3_in_Seg_n_&_ex_y3_being_Element_of_K_st_S2[x3,y3]_)_or_(_not_x3_in_Seg_n_&_ex_y3_being_Element_of_K_st_S2[x3,y3]_)_)
percases ( x3 in Seg n or not x3 in Seg n ) ;
caseA58: x3 in Seg n ; ::_thesis: ex y3 being Element of K st S2[x3,y3]
then  x3 in dom p3 by A52, A54, FINSEQ_1:def_3;
then  ( rng p3 c= the carrier of K & p3 . x3 in rng p3 ) by FINSEQ_1:def_4, FUNCT_1:def_3;
hence  ex y3 being Element of K st S2[x3,y3] by A58; ::_thesis: verum
end;
case not x3 in Seg n ; ::_thesis: ex y3 being Element of K st S2[x3,y3]
hence  ex y3 being Element of K st S2[x3,y3] ; ::_thesis: verum
end;
end;
end;
hence  ex y3 being Element of K st S2[x3,y3] ; ::_thesis: verum
end;
 ex f4 being Function of Ab, the carrier of K st
for x2 being Element of Ab holds S2[x2,f4 . x2] from FUNCT_2:sch_3(A57);
then consider f4 being Function of NAT, the carrier of K such that
A59: for x4 being Element of NAT holds
( ( x4 in Seg n implies f4 . x4 = p3 . x4 ) & ( not x4 in Seg n implies f4 . x4 = 0. K ) ) ;
A60: for n3 being Element of NAT st 0 <> n3 & n3 < len (Path_matrix (p,A)) holds
f4 . (n3 + 1) = the multF of K . ((f4 . n3),((Path_matrix (p,A)) . (n3 + 1)))
proof
let n3 be Element of NAT ; ::_thesis: ( 0 <> n3 & n3 < len (Path_matrix (p,A)) implies f4 . (n3 + 1) = the multF of K . ((f4 . n3),((Path_matrix (p,A)) . (n3 + 1))) )
assume that
A61: 0 <> n3 and
A62: n3 < len (Path_matrix (p,A)) ; ::_thesis: f4 . (n3 + 1) = the multF of K . ((f4 . n3),((Path_matrix (p,A)) . (n3 + 1)))
A63: n3 + 1 <= len (Path_matrix (p,A)) by A62, NAT_1:13;
A64: 0 + 1 <= n3 by A61, NAT_1:13;
then A65: n3 in Seg n by A17, A62;
 1 < n3 + 1 by A64, NAT_1:13;
then  n3 + 1 in Seg n by A17, A63;
then A66: f4 . (n3 + 1) = p3 . (n3 + 1) by A59;
 p3 . (n3 + 1) = the multF of K . ((p3 . n3),((Path_matrix (p,A)) . (n3 + 1))) by A17, A52, A56, A61, A62;
hence  f4 . (n3 + 1) = the multF of K . ((f4 . n3),((Path_matrix (p,A)) . (n3 + 1))) by A59, A66, A65; ::_thesis: verum
end;
A67: i0 <= n by A46, A47, FINSEQ_1:1;
then A68: n -' i0 = n - i0 by XREAL_1:233;
 i0 in dom (Path_matrix (p,A)) by A49, A17, FINSEQ_1:def_3;
then A69: (Path_matrix (p,A)) . i0 = A * (i0,j0) by MATRIX_3:def_7;
defpred S3[ Element of NAT ] means f4 . (i0 + $1) = 0. K;
A70: 0 < i0 by A45, A47, FINSEQ_1:1;
A71: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
A72: 1 <= 1 + (i0 + k) by NAT_1:12;
assume A73: S3[k] ; ::_thesis: S3[k + 1]
now__::_thesis:_(_(_(i0_+_k)_+_1_<=_n_&_S3[k_+_1]_)_or_(_(i0_+_k)_+_1_>_n_&_S3[k_+_1]_)_)
percases ( (i0 + k) + 1 <= n or (i0 + k) + 1 > n ) ;
caseA74: (i0 + k) + 1 <= n ; ::_thesis: S3[k + 1]
 1 <= 1 + (i0 + k) by NAT_1:12;
then  (i0 + k) + 1 in Seg (len (Path_matrix (p,A))) by A17, A74;
then  (i0 + k) + 1 in dom (Path_matrix (p,A)) by FINSEQ_1:def_3;
then A75: (Path_matrix (p,A)) . ((i0 + k) + 1) in rng (Path_matrix (p,A)) by FUNCT_1:def_3;
 rng (Path_matrix (p,A)) c= the carrier of K by FINSEQ_1:def_4;
then reconsider b = (Path_matrix (p,A)) . ((i0 + k) + 1) as Element of K by A75;
 i0 <= i0 + k by NAT_1:12;
then A76: 0 < i0 + k by A45, A47, FINSEQ_1:1;
A77: i0 + k < n by A74, NAT_1:13;
 0 + 1 <= i0 + k by A70, NAT_1:13;
then A78: i0 + k in Seg n by A77;
 (i0 + k) + 1 in Seg n by A72, A74;
then f4 . ((i0 + k) + 1) = p3 . ((i0 + k) + 1) by A59
.= the multF of K . ((p3 . (i0 + k)),((Path_matrix (p,A)) . ((i0 + k) + 1))) by A52, A56, A77, A76
.= (0. K) * b by A59, A73, A78
.= 0. K by VECTSP_1:6 ;
hence  S3[k + 1] ; ::_thesis: verum
end;
case (i0 + k) + 1 > n ; ::_thesis: S3[k + 1]
then  not i0 + (k + 1) in Seg n by FINSEQ_1:1;
hence  S3[k + 1] by A59; ::_thesis: verum
end;
end;
end;
hence  S3[k + 1] ; ::_thesis: verum
end;
 1 in Seg n by A1;
then A79: f4 . 1 = (Path_matrix (p,A)) . 1 by A55, A59;
A80: 1 <= i0 by A45, A47, FINSEQ_1:1;
now__::_thesis:_(_(_i0_<=_1_&_S3[_0_]_)_or_(_i0_>_1_&_S3[_0_]_)_)
percases ( i0 <= 1 or i0 > 1 ) ;
case i0 <= 1 ; ::_thesis: S3[ 0 ]
then  i0 = 1 by A80, XXREAL_0:1;
hence  S3[ 0 ] by A2, A49, A50, A51, A69, A79, Def2; ::_thesis: verum
end;
caseA81: i0 > 1 ; ::_thesis: S3[ 0 ]
reconsider a = f4 . (i0 -' 1) as Element of K ;
 i0 < i0 + 1 by NAT_1:13;
then  i0 - 1 < (i0 + 1) - 1 by XREAL_1:14;
then A82: i0 - 1 < len (Path_matrix (p,A)) by A67, A17, XXREAL_0:2;
 i0 -' 1 = i0 - 1 by A81, XREAL_1:233;
then A83: (i0 -' 1) + 1 = i0 ;
 i0 - 1 > 1 - 1 by A81, XREAL_1:14;
then f4 . i0 = the multF of K . ((f4 . (i0 -' 1)),((Path_matrix (p,A)) . i0)) by A60, A82, A83
.= a * (0. K) by A2, A49, A50, A51, A69, Def2
.= 0. K by VECTSP_1:6 ;
hence  S3[ 0 ] ; ::_thesis: verum
end;
end;
end;
then A84: S3[ 0 ] ;
 for k being Element of NAT holds S3[k] from NAT_1:sch_1(A84, A71);
then  S3[n -' i0] ;
hence  f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p) by A1, A8, A43, A17, A79, A60, A68, FINSOP_1:2; ::_thesis: verum
end;
end;
end;
hence  f2 . p = - (( the multF of K $$ (Path_matrix (p,A))),p) ; ::_thesis: verum
end;
hence  (Path_product A) . x = f2 . x by MATRIX_3:def_8; ::_thesis: verum
end;
deffunc H2( set ) ->  set = IFIN ((idseq n),$1,( the multF of K $$ (diagonal_of_Matrix A)),(0. K));
set F = the addF of K;
set f = Path_product A;
set B = FinOmega (Permutations n);
A85: for x being set st x in Fin (Permutations n) holds
H2(x) in the carrier of K
proof
let x be set ; ::_thesis: ( x in Fin (Permutations n) implies H2(x) in the carrier of K )
assume  x in Fin (Permutations n) ; ::_thesis: H2(x) in the carrier of K
percases ( idseq n in x or not idseq n in x ) ;
suppose idseq n in x ; ::_thesis: H2(x) in the carrier of K
then  H2(x) = the multF of K $$ (diagonal_of_Matrix A) by Def1;
hence  H2(x) in the carrier of K ; ::_thesis: verum
end;
suppose not idseq n in x ; ::_thesis: H2(x) in the carrier of K
then  H2(x) = 0. K by Def1;
hence  H2(x) in the carrier of K ; ::_thesis: verum
end;
end;
end;
 ex f2 being Function of (Fin (Permutations n)), the carrier of K st
for x being set st x in Fin (Permutations n) holds
f2 . x = H2(x) from FUNCT_2:sch_2(A85);
then consider G0 being Function of (Fin (Permutations n)), the carrier of K such that
A86: for x being set st x in Fin (Permutations n) holds
G0 . x = H2(x) ;
 dom f2 = Permutations n by FUNCT_2:def_1;
then A87: dom (Path_product A) = dom f2 by FUNCT_2:def_1;
then A88: Path_product A = f2 by A7, FUNCT_1:2;
A89: for B9 being Element of Fin (Permutations n) st B9 c= FinOmega (Permutations n) & B9 <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product A) . x))
proof
let B9 be Element of Fin (Permutations n); ::_thesis: ( B9 c= FinOmega (Permutations n) & B9 <> {} implies for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product A) . x)) )
assume that
 B9 c= FinOmega (Permutations n) and
 B9 <> {} ; ::_thesis: for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product A) . x))
thus  for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product A) . x)) ::_thesis: verum
proof
let x be Element of Permutations n; ::_thesis: ( x in (FinOmega (Permutations n)) \ B9 implies G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product A) . x)) )
assume A90: x in (FinOmega (Permutations n)) \ B9 ; ::_thesis: G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product A) . x))
A91: now__::_thesis:_(_not_idseq_n_in_B9_\/_{x}_implies_G0_._(B9_\/_{x})_=_0._K_)
assume A92: not idseq n in B9 \/ {x} ; ::_thesis: G0 . (B9 \/ {x}) = 0. K
thus G0 . (B9 \/ {x}) = IFIN ((idseq n),(B9 \/ {.x.}),( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) by A86
.= 0. K by A92, Def1 ; ::_thesis: verum
end;
A93: 0. K is_a_unity_wrt the addF of K by FVSUM_1:6;
A94: now__::_thesis:_(_not_idseq_n_in_B9_implies_G0_._B9_=_0._K_)
assume A95: not idseq n in B9 ; ::_thesis: G0 . B9 = 0. K
thus G0 . B9 = IFIN ((idseq n),B9,( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) by A86
.= 0. K by A95, Def1 ; ::_thesis: verum
end;
A96: now__::_thesis:_(_not_idseq_n_in_B9_\/_{x}_implies_the_addF_of_K_._((G0_._B9),((Path_product_A)_._x))_=_0._K_)
assume A97: not idseq n in B9 \/ {x} ; ::_thesis: the addF of K . ((G0 . B9),((Path_product A) . x)) = 0. K
then  not idseq n in {x} by XBOOLE_0:def_3;
then A98: not idseq n = x by TARSKI:def_1;
(Path_product A) . x = H1(x) by A5, A88
.= 0. K by A98, FUNCOP_1:def_8 ;
hence  the addF of K . ((G0 . B9),((Path_product A) . x)) = 0. K by A94, A93, A97, BINOP_1:3, XBOOLE_0:def_3; ::_thesis: verum
end;
A99: now__::_thesis:_(_idseq_n_in_B9_implies_G0_._B9_=_the_multF_of_K_$$_(diagonal_of_Matrix_A)_)
assume A100: idseq n in B9 ; ::_thesis: G0 . B9 = the multF of K $$ (diagonal_of_Matrix A)
thus G0 . B9 = IFIN ((idseq n),B9,( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) by A86
.= the multF of K $$ (diagonal_of_Matrix A) by A100, Def1 ; ::_thesis: verum
end;
A101: now__::_thesis:_(_idseq_n_in_B9_\/_{x}_implies_the_addF_of_K_._((G0_._B9),((Path_product_A)_._x))_=_the_multF_of_K_$$_(diagonal_of_Matrix_A)_)
assume  idseq n in B9 \/ {x} ; ::_thesis: the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A)
then A102: ( idseq n in B9 or idseq n in {x} ) by XBOOLE_0:def_3;
now__::_thesis:_(_(_idseq_n_in_B9_&_the_addF_of_K_._((G0_._B9),((Path_product_A)_._x))_=_the_multF_of_K_$$_(diagonal_of_Matrix_A)_)_or_(_idseq_n_=_x_&_the_addF_of_K_._((G0_._B9),((Path_product_A)_._x))_=_the_multF_of_K_$$_(diagonal_of_Matrix_A)_)_)
percases ( idseq n in B9 or idseq n = x ) by A102, TARSKI:def_1;
caseA103: idseq n in B9 ; ::_thesis: the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A)
A104: not x in B9 by A90, XBOOLE_0:def_5;
(Path_product A) . x = H1(x) by A5, A88
.= 0. K by A103, A104, FUNCOP_1:def_8 ;
hence  the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A) by A99, A93, A103, BINOP_1:3; ::_thesis: verum
end;
caseA105: idseq n = x ; ::_thesis: the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A)
(Path_product A) . x = H1(x) by A5, A88
.= the multF of K $$ (diagonal_of_Matrix A) by A105, FUNCOP_1:def_8 ;
hence  the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A) by A90, A94, A93, A105, BINOP_1:3, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
hence  the addF of K . ((G0 . B9),((Path_product A) . x)) = the multF of K $$ (diagonal_of_Matrix A) ; ::_thesis: verum
end;
now__::_thesis:_(_idseq_n_in_B9_\/_{x}_implies_G0_._(B9_\/_{x})_=_the_multF_of_K_$$_(diagonal_of_Matrix_A)_)
assume A106: idseq n in B9 \/ {x} ; ::_thesis: G0 . (B9 \/ {x}) = the multF of K $$ (diagonal_of_Matrix A)
thus G0 . (B9 \/ {x}) = IFIN ((idseq n),(B9 \/ {.x.}),( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) by A86
.= the multF of K $$ (diagonal_of_Matrix A) by A106, Def1 ; ::_thesis: verum
end;
hence  G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product A) . x)) by A91, A101, A96; ::_thesis: verum
end;
end;
A107: for x being Element of Permutations n holds G0 . {x} = (Path_product A) . x
proof
let x be Element of Permutations n; ::_thesis: G0 . {x} = (Path_product A) . x
now__::_thesis:_(_(_x_=_idseq_n_&_G0_._{.x.}_=_f2_._x_)_or_(_x_<>_idseq_n_&_G0_._{.x.}_=_f2_._x_)_)
percases ( x = idseq n or x <> idseq n ) ;
caseA108: x = idseq n ; ::_thesis: G0 . {.x.} = f2 . x
then  idseq n in {x} by TARSKI:def_1;
then A109: IFIN ((idseq n),{x},( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) = the multF of K $$ (diagonal_of_Matrix A) by Def1;
f2 . x = H1(x) by A5
.= the multF of K $$ (diagonal_of_Matrix A) by A108, FUNCOP_1:def_8 ;
hence  G0 . {.x.} = f2 . x by A86, A109; ::_thesis: verum
end;
caseA110: x <> idseq n ; ::_thesis: G0 . {.x.} = f2 . x
then  not idseq n in {x} by TARSKI:def_1;
then A111: IFIN ((idseq n),{x},( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) = 0. K by Def1;
f2 . x = H1(x) by A5
.= 0. K by A110, FUNCOP_1:def_8 ;
hence  G0 . {.x.} = f2 . x by A86, A111; ::_thesis: verum
end;
end;
end;
hence  G0 . {x} = (Path_product A) . x by A87, A7, FUNCT_1:2; ::_thesis: verum
end;
A112: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G0 . {} = e
proof
let e be Element of the carrier of K; ::_thesis: ( e is_a_unity_wrt the addF of K implies G0 . {} = e )
assume  e is_a_unity_wrt the addF of K ; ::_thesis: G0 . {} = e
then A113: the addF of K . ((0. K),e) = 0. K by BINOP_1:3;
 0. K is_a_unity_wrt the addF of K by FVSUM_1:6;
then A114: the addF of K . ((0. K),e) = e by BINOP_1:3;
 IFIN ((idseq n),{},( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) = 0. K by Def1;
hence  G0 . {} = e by A86, A113, A114, FINSUB_1:7; ::_thesis: verum
end;
A115: now__::_thesis:_(_idseq_n_in_FinOmega_(Permutations_n)_implies_G0_._(FinOmega_(Permutations_n))_=_the_multF_of_K_$$_(diagonal_of_Matrix_A)_)
assume A116: idseq n in FinOmega (Permutations n) ; ::_thesis: G0 . (FinOmega (Permutations n)) = the multF of K $$ (diagonal_of_Matrix A)
thus G0 . (FinOmega (Permutations n)) = IFIN ((idseq n),(FinOmega (Permutations n)),( the multF of K $$ (diagonal_of_Matrix A)),(0. K)) by A86
.= the multF of K $$ (diagonal_of_Matrix A) by A116, Def1 ; ::_thesis: verum
end;
 idseq n is Element of (Group_of_Perm n) by MATRIX_2:20;
then  ( FinOmega (Permutations n) = Permutations n & idseq n in the carrier of (Group_of_Perm n) ) by MATRIX_2:26, MATRIX_2:def_14;
then  the addF of K $$ ((FinOmega (Permutations n)),(Path_product A)) = the multF of K $$ (diagonal_of_Matrix A) by A115, A112, A107, A89, MATRIX_2:def_10, SETWISEO:def_3;
hence  Det A = the multF of K $$ (diagonal_of_Matrix A) by MATRIX_3:def_9; ::_thesis: verum
end;

theorem Th18: :: MATRIX_7:18
for n being Nat
for p being Element of Permutations n holds p " is Element of Permutations n
proof
let n be Nat; ::_thesis: for p being Element of Permutations n holds p " is Element of Permutations n
let p be Element of Permutations n; ::_thesis: p " is Element of Permutations n
 p " is Element of (Group_of_Perm n) by MATRIX_2:23;
hence  p " is Element of Permutations n by MATRIX_2:def_10; ::_thesis: verum
end;

definition
let n be Nat;
let p be Element of Permutations n;
:: original: "
redefine funcp "  ->  Element of Permutations n;
coherence
 p " is Element of Permutations n by Th18;
end;

theorem Th19: :: MATRIX_7:19
for n being Nat
for K being Field
for A being Matrix of n,K holds A @ is Matrix of n,K ;

theorem :: MATRIX_7:20
for G being Group
for f1, f2 being FinSequence of G holds (Product (f1 ^ f2)) " = ((Product f2) ") * ((Product f1) ")
proof
let G be Group; ::_thesis: for f1, f2 being FinSequence of G holds (Product (f1 ^ f2)) " = ((Product f2) ") * ((Product f1) ")
let f1, f2 be FinSequence of G; ::_thesis: (Product (f1 ^ f2)) " = ((Product f2) ") * ((Product f1) ")
thus (Product (f1 ^ f2)) " = ((Product f1) * (Product f2)) " by GROUP_4:5
.= ((Product f2) ") * ((Product f1) ") by GROUP_1:17 ; ::_thesis: verum
end;

definition
let G be Group;
let f be FinSequence of G;
canceled;
funcf "  ->  FinSequence of G means :Def4: :: MATRIX_7:def 4
( len it = len f & ( for i being Element of NAT st i in dom f holds
it /. i = (f /. i) " ) );
existence
 ex b1 being FinSequence of G st
( len b1 = len f & ( for i being Element of NAT st i in dom f holds
b1 /. i = (f /. i) " ) )
proof
deffunc H1( Nat) ->  Element of the carrier of G = (f /. $1) " ;
 ex p being FinSequence st
( len p = len f & ( for k being Nat st k in dom p holds
p . k = H1(k) ) ) from FINSEQ_1:sch_2();
then consider p being FinSequence such that
A1: len p = len f and
A2: for k being Nat st k in dom p holds
p . k = H1(k) ;
 rng p c= the carrier of G
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in the carrier of G )
assume  y in rng p ; ::_thesis: y in the carrier of G
then consider x being set  such that
A3: x in dom p and
A4: y = p . x by FUNCT_1:def_3;
reconsider k = x as Element of NAT by A3;
 p . k = (f /. k) " by A2, A3;
hence  y in the carrier of G by A4; ::_thesis: verum
end;
then reconsider q = p as FinSequence of G by FINSEQ_1:def_4;
A5: dom p = dom f by A1, FINSEQ_3:29;
 for i being Element of NAT st i in dom f holds
q /. i = (f /. i) "
proof
let i be Element of NAT ; ::_thesis: ( i in dom f implies q /. i = (f /. i) " )
assume A6: i in dom f ; ::_thesis: q /. i = (f /. i) "
hence q /. i = p . i by A5, PARTFUN1:def_6
.= (f /. i) " by A2, A5, A6 ;
::_thesis: verum
end;
hence  ex b1 being FinSequence of G st
( len b1 = len f & ( for i being Element of NAT st i in dom f holds
b1 /. i = (f /. i) " ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of G st len b1 = len f & ( for i being Element of NAT st i in dom f holds
b1 /. i = (f /. i) " ) & len b2 = len f & ( for i being Element of NAT st i in dom f holds
b2 /. i = (f /. i) " ) holds
b1 = b2
proof
thus  for g1, g2 being FinSequence of G st len g1 = len f & ( for i being Element of NAT st i in dom f holds
g1 /. i = (f /. i) " ) & len g2 = len f & ( for j being Element of NAT st j in dom f holds
g2 /. j = (f /. j) " ) holds
g1 = g2 ::_thesis: verum
proof
let g1, g2 be FinSequence of G; ::_thesis: ( len g1 = len f & ( for i being Element of NAT st i in dom f holds
g1 /. i = (f /. i) " ) & len g2 = len f & ( for j being Element of NAT st j in dom f holds
g2 /. j = (f /. j) " ) implies g1 = g2 )
assume that
A7: len g1 = len f and
A8: for i being Element of NAT st i in dom f holds
g1 /. i = (f /. i) " and
A9: len g2 = len f and
A10: for j being Element of NAT st j in dom f holds
g2 /. j = (f /. j) " ; ::_thesis: g1 = g2
A11: dom g1 = dom f by A7, FINSEQ_3:29;
 for k being Nat st 1 <= k & k <= len g1 holds
g1 . k = g2 . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len g1 implies g1 . k = g2 . k )
assume A12: ( 1 <= k & k <= len g1 ) ; ::_thesis: g1 . k = g2 . k
A13: k in NAT by ORDINAL1:def_12;
then  k in Seg (len g2) by A7, A9, A12;
then  k in dom g2 by FINSEQ_1:def_3;
then A14: g2 . k = g2 /. k by PARTFUN1:def_6;
 k in Seg (len g1) by A13, A12;
then A15: k in dom g1 by FINSEQ_1:def_3;
then  ( g1 . k = g1 /. k & g1 /. k = (f /. k) " ) by A8, A11, PARTFUN1:def_6;
hence  g1 . k = g2 . k by A10, A11, A15, A14; ::_thesis: verum
end;
hence  g1 = g2 by A7, A9, FINSEQ_1:14; ::_thesis: verum
end;
end;
end;

:: deftheorem  MATRIX_7:def_3_:_
canceled;

:: deftheorem Def4 defines " MATRIX_7:def_4_:_
 for G being Group
for f, b3 being FinSequence of G holds
( b3 = f " iff ( len b3 = len f & ( for i being Element of NAT st i in dom f holds
b3 /. i = (f /. i) " ) ) );

theorem Th21: :: MATRIX_7:21
for G being Group holds (<*> the carrier of G) " = <*> the carrier of G
proof
let G be Group; ::_thesis: (<*> the carrier of G) " = <*> the carrier of G
 len (<*> the carrier of G) = 0 ;
then  len ((<*> the carrier of G) ") = 0 by Def4;
hence  (<*> the carrier of G) " = <*> the carrier of G ; ::_thesis: verum
end;

theorem Th22: :: MATRIX_7:22
for G being Group
for f, g being FinSequence of G holds (f ^ g) " = (f ") ^ (g ")
proof
let G be Group; ::_thesis: for f, g being FinSequence of G holds (f ^ g) " = (f ") ^ (g ")
let f, g be FinSequence of G; ::_thesis: (f ^ g) " = (f ") ^ (g ")
A1: len ((f ^ g) ") = len (f ^ g) by Def4
.= (len f) + (len g) by FINSEQ_1:22 ;
A2: (len f) + (len g) = (len (f ")) + (len g) by Def4
.= (len (f ")) + (len (g ")) by Def4
.= len ((f ") ^ (g ")) by FINSEQ_1:22 ;
A3: len ((f ^ g) ") = len (f ^ g) by Def4;
 for i being Nat st 1 <= i & i <= len ((f ^ g) ") holds
((f ^ g) ") . i = ((f ") ^ (g ")) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len ((f ^ g) ") implies ((f ^ g) ") . i = ((f ") ^ (g ")) . i )
assume that
A4: 1 <= i and
A5: i <= len ((f ^ g) ") ; ::_thesis: ((f ^ g) ") . i = ((f ") ^ (g ")) . i
A6: i in NAT by ORDINAL1:def_12;
now__::_thesis:_(_(_len_f_>_0_&_((f_^_g)_")_._i_=_((f_")_^_(g_"))_._i_)_or_(_len_f_<=_0_&_((f_^_g)_")_._i_=_((f_")_^_(g_"))_._i_)_)
percases ( len f > 0 or len f <= 0 ) ;
case len f > 0 ; ::_thesis: ((f ^ g) ") . i = ((f ") ^ (g ")) . i
A7: len (f ") = len f by Def4;
 len ((f ^ g) ") = len (f ^ g) by Def4;
then A8: dom ((f ^ g) ") = dom (f ^ g) by FINSEQ_3:29;
 i in Seg (len ((f ^ g) ")) by A4, A5, A6;
then A9: i in dom ((f ^ g) ") by FINSEQ_1:def_3;
then A10: ((f ^ g) ") . i = ((f ^ g) ") /. i by PARTFUN1:def_6
.= ((f ^ g) /. i) " by A8, A9, Def4 ;
A11: len (g ") = len g by Def4;
now__::_thesis:_(_(_i_<=_len_f_&_((f_^_g)_")_._i_=_((f_")_^_(g_"))_._i_)_or_(_i_>_len_f_&_((f_^_g)_")_._i_=_((f_")_^_(g_"))_._i_)_)
percases ( i <= len f or i > len f ) ;
case i <= len f ; ::_thesis: ((f ^ g) ") . i = ((f ") ^ (g ")) . i
then A12: i in Seg (len f) by A4, A6;
then A13: i in dom f by FINSEQ_1:def_3;
A14: i in dom (f ") by A7, A12, FINSEQ_1:def_3;
(f ^ g) /. i = (f ^ g) . i by A8, A9, PARTFUN1:def_6
.= f . i by A13, FINSEQ_1:def_7
.= f /. i by A13, PARTFUN1:def_6 ;
then ((f ^ g) /. i) " = (f ") /. i by A13, Def4
.= (f ") . i by A14, PARTFUN1:def_6 ;
hence  ((f ^ g) ") . i = ((f ") ^ (g ")) . i by A10, A14, FINSEQ_1:def_7; ::_thesis: verum
end;
caseA15: i > len f ; ::_thesis: ((f ^ g) ") . i = ((f ") ^ (g ")) . i
then  1 + (len f) <= i by NAT_1:13;
then A16: (1 + (len f)) - (len f) <= i - (len f) by XREAL_1:9;
A17: i -' (len f) = i - (len f) by A15, XREAL_1:233;
 i - (len f) <= ((len g) + (len f)) - (len f) by A1, A5, XREAL_1:9;
then A18: i -' (len f) in Seg (len g) by A17, A16;
then A19: i -' (len f) in dom g by FINSEQ_1:def_3;
A20: i -' (len f) in dom (g ") by A11, A18, FINSEQ_1:def_3;
(f ^ g) /. i = (f ^ g) . i by A8, A9, PARTFUN1:def_6
.= g . (i - (len f)) by A3, A5, A15, FINSEQ_1:24
.= g /. (i -' (len f)) by A17, A19, PARTFUN1:def_6 ;
then ((f ^ g) /. i) " = (g ") /. (i -' (len f)) by A19, Def4
.= (g ") . (i - (len (f "))) by A7, A17, A20, PARTFUN1:def_6 ;
hence  ((f ^ g) ") . i = ((f ") ^ (g ")) . i by A1, A2, A5, A7, A10, A15, FINSEQ_1:24; ::_thesis: verum
end;
end;
end;
hence  ((f ^ g) ") . i = ((f ") ^ (g ")) . i ; ::_thesis: verum
end;
case len f <= 0 ; ::_thesis: ((f ^ g) ") . i = ((f ") ^ (g ")) . i
then  f = {} ;
then  ( (f ^ g) " = g " & f " = <*> the carrier of G ) by Th21, FINSEQ_1:34;
hence  ((f ^ g) ") . i = ((f ") ^ (g ")) . i by FINSEQ_1:34; ::_thesis: verum
end;
end;
end;
hence  ((f ^ g) ") . i = ((f ") ^ (g ")) . i ; ::_thesis: verum
end;
hence  (f ^ g) " = (f ") ^ (g ") by A1, A2, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th23: :: MATRIX_7:23
for G being Group
for a being Element of G holds <*a*> " = <*(a ")*>
proof
let G be Group; ::_thesis: for a being Element of G holds <*a*> " = <*(a ")*>
let a be Element of G; ::_thesis: <*a*> " = <*(a ")*>
A1: len (<*a*> ") = len <*a*> by Def4
.= 1 by FINSEQ_1:39
.= len <*(a ")*> by FINSEQ_1:39 ;
 for i being Nat st 1 <= i & i <= len <*(a ")*> holds
(<*a*> ") . i = <*(a ")*> . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len <*(a ")*> implies (<*a*> ") . i = <*(a ")*> . i )
assume A2: ( 1 <= i & i <= len <*(a ")*> ) ; ::_thesis: (<*a*> ") . i = <*(a ")*> . i
A3: len <*(a ")*> = 1 by FINSEQ_1:39;
then A4: i = 1 by A2, XXREAL_0:1;
A5: i in NAT by ORDINAL1:def_12;
 len <*a*> = 1 by FINSEQ_1:39;
then  i in Seg (len <*a*>) by A2, A5, A3;
then A6: i in dom <*a*> by FINSEQ_1:def_3;
 i in Seg (len (<*a*> ")) by A1, A2, A5;
then  i in dom (<*a*> ") by FINSEQ_1:def_3;
then A7: (<*a*> ") . i = (<*a*> ") /. i by PARTFUN1:def_6
.= (<*a*> /. i) " by A6, Def4 ;
<*a*> /. i = <*a*> . i by A6, PARTFUN1:def_6
.= a by A4, FINSEQ_1:40 ;
hence  (<*a*> ") . i = <*(a ")*> . i by A4, A7, FINSEQ_1:40; ::_thesis: verum
end;
hence  <*a*> " = <*(a ")*> by A1, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th24: :: MATRIX_7:24
for G being Group
for f being FinSequence of G holds Product (f ^ ((Rev f) ")) = 1_ G
proof
let G be Group; ::_thesis: for f being FinSequence of G holds Product (f ^ ((Rev f) ")) = 1_ G
let f be FinSequence of G; ::_thesis: Product (f ^ ((Rev f) ")) = 1_ G
defpred S1[ Element of NAT ] means  for g being FinSequence of G st len g <= $1 holds
Product (g ^ ((Rev g) ")) = 1_ G;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
 for g being FinSequence of G st len g <= k + 1 holds
Product (g ^ ((Rev g) ")) = 1_ G
proof
let g be FinSequence of G; ::_thesis: ( len g <= k + 1 implies Product (g ^ ((Rev g) ")) = 1_ G )
assume A3: len g <= k + 1 ; ::_thesis: Product (g ^ ((Rev g) ")) = 1_ G
now__::_thesis:_(_(_len_g_<_k_+_1_&_Product_(g_^_((Rev_g)_"))_=_1__G_)_or_(_len_g_=_k_+_1_&_Product_(g_^_((Rev_g)_"))_=_1__G_)_)
percases ( len g < k + 1 or len g = k + 1 ) by A3, XXREAL_0:1;
case len g < k + 1 ; ::_thesis: Product (g ^ ((Rev g) ")) = 1_ G
then  len g <= k by NAT_1:13;
hence  Product (g ^ ((Rev g) ")) = 1_ G by A2; ::_thesis: verum
end;
caseA4: len g = k + 1 ; ::_thesis: Product (g ^ ((Rev g) ")) = 1_ G
reconsider h = g | k as FinSequence of G ;
 k < len g by A4, NAT_1:13;
then A5: len h = k by FINSEQ_1:59;
A6: Product (<*(g /. (k + 1))*> ^ (<*(g /. (k + 1))*> ")) = (Product <*(g /. (k + 1))*>) * (Product (<*(g /. (k + 1))*> ")) by GROUP_4:5
.= (g /. (k + 1)) * (Product (<*(g /. (k + 1))*> ")) by FINSOP_1:11
.= (g /. (k + 1)) * (Product <*((g /. (k + 1)) ")*>) by Th23
.= (g /. (k + 1)) * ((g /. (k + 1)) ") by FINSOP_1:11
.= 1_ G by GROUP_1:def_5 ;
A7: g = h ^ <*(g /. (k + 1))*> by A4, FINSEQ_5:21;
then  Rev g = <*(g /. (k + 1))*> ^ (Rev h) by FINSEQ_5:63;
then  (Rev g) " = (<*(g /. (k + 1))*> ") ^ ((Rev h) ") by Th22;
then g ^ ((Rev g) ") = h ^ (<*(g /. (k + 1))*> ^ ((<*(g /. (k + 1))*> ") ^ ((Rev h) "))) by A7, FINSEQ_1:32
.= h ^ ((<*(g /. (k + 1))*> ^ (<*(g /. (k + 1))*> ")) ^ ((Rev h) ")) by FINSEQ_1:32 ;
then  Product (g ^ ((Rev g) ")) = (Product h) * (Product ((<*(g /. (k + 1))*> ^ (<*(g /. (k + 1))*> ")) ^ ((Rev h) "))) by GROUP_4:5
.= (Product h) * ((Product (<*(g /. (k + 1))*> ^ (<*(g /. (k + 1))*> "))) * (Product ((Rev h) "))) by GROUP_4:5
.= (Product h) * (Product ((Rev h) ")) by A6, GROUP_1:def_4
.= Product (h ^ ((Rev h) ")) by GROUP_4:5 ;
hence  Product (g ^ ((Rev g) ")) = 1_ G by A2, A5; ::_thesis: verum
end;
end;
end;
hence  Product (g ^ ((Rev g) ")) = 1_ G ; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for g being FinSequence of G st len g <= 0 holds
Product (g ^ ((Rev g) ")) = 1_ G
proof
let g be FinSequence of G; ::_thesis: ( len g <= 0 implies Product (g ^ ((Rev g) ")) = 1_ G )
assume  len g <= 0 ; ::_thesis: Product (g ^ ((Rev g) ")) = 1_ G
then A8: g = <*> the carrier of G ;
then  Rev g = <*> the carrier of G by FINSEQ_5:79;
then  (Rev g) " = <*> the carrier of G by Th21;
then  g ^ ((Rev g) ") = <*> the carrier of G by A8, FINSEQ_1:34;
hence  Product (g ^ ((Rev g) ")) = 1_ G by GROUP_4:8; ::_thesis: verum
end;
then A9: S1[ 0 ] ;
 for j being Element of NAT holds S1[j] from NAT_1:sch_1(A9, A1);
then  S1[ len f] ;
hence  Product (f ^ ((Rev f) ")) = 1_ G ; ::_thesis: verum
end;

theorem Th25: :: MATRIX_7:25
for G being Group
for f being FinSequence of G holds Product (((Rev f) ") ^ f) = 1_ G
proof
let G be Group; ::_thesis: for f being FinSequence of G holds Product (((Rev f) ") ^ f) = 1_ G
let f be FinSequence of G; ::_thesis: Product (((Rev f) ") ^ f) = 1_ G
A1: len f = len (Rev f) by FINSEQ_5:def_3;
A2: len (Rev ((Rev f) ")) = len ((Rev ((Rev f) ")) ") by Def4;
then A3: dom (Rev ((Rev f) ")) = dom ((Rev ((Rev f) ")) ") by FINSEQ_3:29;
A4: len ((Rev f) ") = len (Rev ((Rev f) ")) by FINSEQ_5:def_3;
A5: len (Rev f) = len ((Rev f) ") by Def4;
then A6: dom (Rev f) = dom ((Rev f) ") by FINSEQ_3:29;
 for i being Nat st 1 <= i & i <= len f holds
f . i = ((Rev ((Rev f) ")) ") . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies f . i = ((Rev ((Rev f) ")) ") . i )
assume that
A7: 1 <= i and
A8: i <= len f ; ::_thesis: f . i = ((Rev ((Rev f) ")) ") . i
 ((len f) - i) + 1 = ((len f) -' i) + 1 by A8, XREAL_1:233;
then reconsider j = ((len f) - i) + 1 as Element of NAT ;
A9: i + j = (len f) + 1 ;
 i in NAT by ORDINAL1:def_12;
then A10: i in Seg (len f) by A7, A8;
then A11: i in dom ((Rev ((Rev f) ")) ") by A1, A5, A4, A2, FINSEQ_1:def_3;
 i - 1 >= 0 by A7, XREAL_1:48;
then  (len f) + 0 <= (len f) + (i - 1) by XREAL_1:7;
then A12: (len f) - (i - 1) <= ((len f) + (i - 1)) - (i - 1) by XREAL_1:13;
 (len f) - i = (len f) -' i by A8, XREAL_1:233;
then  ((len f) - i) + 1 >= 0 + 1 by XREAL_1:6;
then  j in Seg (len f) by A12;
then A13: j in dom ((Rev f) ") by A1, A5, FINSEQ_1:def_3;
A14: j + i = (len f) + 1 ;
A15: i in dom f by A10, FINSEQ_1:def_3;
then f . i = f /. i by PARTFUN1:def_6
.= (Rev f) /. j by A15, A9, FINSEQ_5:66
.= (((Rev f) /. j) ") "
.= (((Rev f) ") /. j) " by A6, A13, Def4
.= ((Rev ((Rev f) ")) /. i) " by A1, A5, A13, A14, FINSEQ_5:66
.= ((Rev ((Rev f) ")) ") /. i by A3, A11, Def4
.= ((Rev ((Rev f) ")) ") . i by A11, PARTFUN1:def_6 ;
hence  f . i = ((Rev ((Rev f) ")) ") . i ; ::_thesis: verum
end;
then  (Rev ((Rev f) ")) " = f by A1, A5, A4, A2, FINSEQ_1:14;
hence  Product (((Rev f) ") ^ f) = 1_ G by Th24; ::_thesis: verum
end;

theorem Th26: :: MATRIX_7:26
for G being Group
for f being FinSequence of G holds (Product f) " = Product ((Rev f) ")
proof
let G be Group; ::_thesis: for f being FinSequence of G holds (Product f) " = Product ((Rev f) ")
let f be FinSequence of G; ::_thesis: (Product f) " = Product ((Rev f) ")
 Product (f ^ ((Rev f) ")) = 1_ G by Th24;
then A1: (Product f) * (Product ((Rev f) ")) = 1_ G by GROUP_4:5;
 Product (((Rev f) ") ^ f) = 1_ G by Th25;
then  (Product ((Rev f) ")) * (Product f) = 1_ G by GROUP_4:5;
hence  (Product f) " = Product ((Rev f) ") by A1, GROUP_1:5; ::_thesis: verum
end;

theorem Th27: :: MATRIX_7:27
for n being Nat
for ITP being Element of Permutations n
for ITG being Element of (Group_of_Perm n) st ITG = ITP & n >= 1 holds
ITP " = ITG "
proof
let n be Nat; ::_thesis: for ITP being Element of Permutations n
for ITG being Element of (Group_of_Perm n) st ITG = ITP & n >= 1 holds
ITP " = ITG "
let ITP be Element of Permutations n; ::_thesis: for ITG being Element of (Group_of_Perm n) st ITG = ITP & n >= 1 holds
ITP " = ITG "
let ITG be Element of (Group_of_Perm n); ::_thesis: ( ITG = ITP & n >= 1 implies ITP " = ITG " )
assume that
A1: ITG = ITP and
A2: n >= 1 ; ::_thesis: ITP " = ITG "
reconsider qf = ITP as Function of (Seg n),(Seg n) by MATRIX_2:def_9;
 dom qf = Seg n by A2, FUNCT_2:def_1;
then A3: (ITP ") * ITP = id (Seg n) by FUNCT_1:39;
 ITP is Permutation of (Seg n) by MATRIX_2:def_9;
then  rng qf = Seg n by FUNCT_2:def_3;
then A4: ITP * (ITP ") = id (Seg n) by FUNCT_1:39;
reconsider pf = ITP " as Element of (Group_of_Perm n) by MATRIX_2:def_10;
A5: ( idseq n = 1_ (Group_of_Perm n) & ITG * pf = the multF of (Group_of_Perm n) . (ITG,pf) ) by MATRIX_2:24;
A6: pf * ITG = the multF of (Group_of_Perm n) . (pf,ITG) ;
 ( the multF of (Group_of_Perm n) . (ITG,pf) = (ITP ") * ITP & the multF of (Group_of_Perm n) . (pf,ITG) = ITP * (ITP ") ) by A1, MATRIX_2:def_10;
hence  ITP " = ITG " by A3, A4, A5, A6, GROUP_1:def_5; ::_thesis: verum
end;

Lm2:  for n being Element of NAT
for IT being Element of Permutations n st IT is even & n >= 1 holds
IT " is even
proof
let n be Element of NAT ; ::_thesis: for IT being Element of Permutations n st IT is even & n >= 1 holds
IT " is even
let IT be Element of Permutations n; ::_thesis: ( IT is even & n >= 1 implies IT " is even )
assume that
A1: IT is even and
A2: n >= 1 ; ::_thesis: IT " is even
reconsider ITP = IT as Element of Permutations n ;
reconsider ITG = ITP as Element of (Group_of_Perm n) by MATRIX_2:def_10;
A3: len (Permutations n) = n by MATRIX_2:18;
then consider l being FinSequence of (Group_of_Perm n) such that
A4: (len l) mod 2 = 0 and
A5: IT = Product l and
A6: 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 ) by A1, MATRIX_2:def_12;
set m = len l;
reconsider lv = (Rev l) " as FinSequence of (Group_of_Perm n) ;
A7: len l = len (Rev l) by FINSEQ_5:def_3;
then A8: len l = len lv by Def4;
A9: for i being Nat st i in dom lv holds
ex q2 being Element of Permutations n st
( lv . i = q2 & q2 is being_transposition )
proof
let i be Nat; ::_thesis: ( i in dom lv implies ex q2 being Element of Permutations n st
( lv . i = q2 & q2 is being_transposition ) )
reconsider ii = i as Element of NAT by ORDINAL1:def_12;
assume A10: i in dom lv ; ::_thesis: ex q2 being Element of Permutations n st
( lv . i = q2 & q2 is being_transposition )
then A11: i in dom (Rev l) by A7, A8, FINSEQ_3:29;
A12: i in Seg (len lv) by A10, FINSEQ_1:def_3;
then  1 <= i by FINSEQ_1:1;
then  (len l) + 1 <= (len l) + i by XREAL_1:7;
then A13: ((len l) + 1) - i <= ((len l) + i) - i by XREAL_1:9;
 i <= len l by A8, A12, FINSEQ_1:1;
then A14: (len l) - i >= 0 by XREAL_1:48;
then  ((len l) - i) + 1 = ((len l) -' i) + 1 by XREAL_0:def_2;
then reconsider j = ((len l) - i) + 1 as Element of NAT ;
 ((len l) - i) + 1 >= 0 + 1 by A14, XREAL_1:7;
then  j in Seg (len l) by A13;
then A15: j in dom l by FINSEQ_1:def_3;
then consider q being Element of Permutations n such that
A16: l . j = q and
A17: q is being_transposition by A6;
 lv . i = lv /. i by A10, PARTFUN1:def_6;
then reconsider qq = lv . i as Element of Permutations n by MATRIX_2:def_10;
reconsider qqf = qq as Function of (Seg n),(Seg n) by MATRIX_2:def_9;
A18: i + j = (len l) + 1 ;
reconsider qf = q as Function of (Seg n),(Seg n) by MATRIX_2:def_9;
consider i1, j1 being Nat such that
A19: ( i1 in dom q & j1 in dom q & i1 <> j1 & q . i1 = j1 & q . j1 = i1 ) and
A20: for k being Nat st k <> i1 & k <> j1 & k in dom q holds
q . k = k by A17, MATRIX_2:def_11;
A21: ( dom qf = Seg n & dom qqf = Seg n ) by A2, FUNCT_2:def_1;
A22: qq = ((Rev l) ") /. i by A10, PARTFUN1:def_6
.= ((Rev l) /. ii) " by A11, Def4
.= (l /. j) " by A18, A15, FINSEQ_5:66
.= q " by A2, A15, A16, Th27, PARTFUN1:def_6 ;
A23: for k being Element of NAT st k <> j1 & k <> i1 & k in dom qq holds
qq . k = k
proof
let k be Element of NAT ; ::_thesis: ( k <> j1 & k <> i1 & k in dom qq implies qq . k = k )
assume that
A24: ( k <> j1 & k <> i1 ) and
A25: k in dom qq ; ::_thesis: qq . k = k
 q . k = k by A20, A21, A24, A25;
hence  qq . k = k by A21, A22, A25, FUNCT_1:32; ::_thesis: verum
end;
A26: qq = ((Rev l) ") /. i by A10, PARTFUN1:def_6
.= ((Rev l) /. ii) " by A11, Def4
.= (l /. j) " by A18, A15, FINSEQ_5:66
.= q " by A2, A15, A16, Th27, PARTFUN1:def_6 ;
 ex i, j being Nat st
( i in dom qq & j in dom qq & i <> j & qq . i = j & qq . j = i & ( for k being Nat st k <> i & k <> j & k in dom qq holds
qq . k = k ) )
proof
take i = i1; ::_thesis: ex j being Nat st
( i in dom qq & j in dom qq & i <> j & qq . i = j & qq . j = i & ( for k being Nat st k <> i & k <> j & k in dom qq holds
qq . k = k ) )
take j = j1; ::_thesis: ( i in dom qq & j in dom qq & i <> j & qq . i = j & qq . j = i & ( for k being Nat st k <> i & k <> j & k in dom qq holds
qq . k = k ) )
thus  ( i in dom qq & j in dom qq & i <> j & qq . i = j & qq . j = i ) by A19, A21, A26, FUNCT_1:32; ::_thesis: for k being Nat st k <> i & k <> j & k in dom qq holds
qq . k = k
let k be Nat; ::_thesis: ( k <> i & k <> j & k in dom qq implies qq . k = k )
 k in NAT by ORDINAL1:def_12;
hence  ( k <> i & k <> j & k in dom qq implies qq . k = k ) by A23; ::_thesis: verum
end;
then  qq is being_transposition by MATRIX_2:def_11;
hence  ex q2 being Element of Permutations n st
( lv . i = q2 & q2 is being_transposition ) ; ::_thesis: verum
end;
 ITG " = ITP " by A2, Th27;
then  IT " = Product lv by A5, Th26;
hence  IT " is even by A3, A4, A8, A9, MATRIX_2:def_12; ::_thesis: verum
end;

theorem Th28: :: MATRIX_7:28
for n being Element of NAT
for IT being Element of Permutations n st n >= 1 holds
( IT is even iff IT " is even )
proof
let n be Element of NAT ; ::_thesis: for IT being Element of Permutations n st n >= 1 holds
( IT is even iff IT " is even )
let IT be Element of Permutations n; ::_thesis: ( n >= 1 implies ( IT is even iff IT " is even ) )
assume A1: n >= 1 ; ::_thesis: ( IT is even iff IT " is even )
hence  ( IT is even implies IT " is even ) by Lm2; ::_thesis: ( IT " is even implies IT is even )
now__::_thesis:_(_IT_"_is_even_implies_IT_is_even_)
assume  IT " is even ; ::_thesis: IT is even
then  (IT ") " is even by A1, Lm2;
hence  IT is even by FUNCT_1:43; ::_thesis: verum
end;
hence  ( IT " is even implies IT is even ) ; ::_thesis: verum
end;

theorem Th29: :: MATRIX_7:29
for n being Element of NAT
for K being Field
for p being Element of Permutations n
for x being Element of K st n >= 1 holds
- (x,p) = - (x,(p "))
proof
let n be Element of NAT ; ::_thesis: for K being Field
for p being Element of Permutations n
for x being Element of K st n >= 1 holds
- (x,p) = - (x,(p "))
let K be Field; ::_thesis: for p being Element of Permutations n
for x being Element of K st n >= 1 holds
- (x,p) = - (x,(p "))
let p be Element of Permutations n; ::_thesis: for x being Element of K st n >= 1 holds
- (x,p) = - (x,(p "))
let x be Element of K; ::_thesis: ( n >= 1 implies - (x,p) = - (x,(p ")) )
assume A1: n >= 1 ; ::_thesis: - (x,p) = - (x,(p "))
reconsider pf = p as Permutation of (Seg n) by MATRIX_2:def_9;
A2: len (Permutations n) = n by MATRIX_2:18;
percases ( p is even or not p is even ) ;
suppose p is even ; ::_thesis: - (x,p) = - (x,(p "))
then  ( - (x,p) = x & pf " is even ) by A1, A2, Th28, MATRIX_2:def_13;
hence  - (x,p) = - (x,(p ")) by A2, MATRIX_2:def_13; ::_thesis: verum
end;
suppose not p is even ; ::_thesis: - (x,p) = - (x,(p "))
then  ( - (x,p) = - x & not p " is even ) by A1, Th28, MATRIX_2:def_13;
hence  - (x,p) = - (x,(p ")) by MATRIX_2:def_13; ::_thesis: verum
end;
end;
end;

theorem :: MATRIX_7:30
for K being Field
for f1, f2 being FinSequence of K holds the multF of K $$ (f1 ^ f2) = ( the multF of K $$ f1) * ( the multF of K $$ f2) by FINSOP_1:5;

theorem Th31: :: MATRIX_7:31
for K being Field
for R1, R2 being FinSequence of K st R1,R2 are_fiberwise_equipotent holds
the multF of K $$ R1 = the multF of K $$ R2
proof
let K be Field; ::_thesis: for R1, R2 being FinSequence of K st R1,R2 are_fiberwise_equipotent holds
the multF of K $$ R1 = the multF of K $$ R2
defpred S1[ Nat] means  for f, g being FinSequence of K st f,g are_fiberwise_equipotent & len f = $1 holds
the multF of K $$ f = the multF of K $$ g;
let R1, R2 be FinSequence of K; ::_thesis: ( R1,R2 are_fiberwise_equipotent implies the multF of K $$ R1 = the multF of K $$ R2 )
assume A1: R1,R2 are_fiberwise_equipotent ; ::_thesis: the multF of K $$ R1 = the multF of K $$ R2
A2: len R1 = len R1 ;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
let f, g be FinSequence of K; ::_thesis: ( f,g are_fiberwise_equipotent & len f = n + 1 implies the multF of K $$ f = the multF of K $$ g )
assume that
A5: f,g are_fiberwise_equipotent and
A6: len f = n + 1 ; ::_thesis: the multF of K $$ f = the multF of K $$ g
A7: rng f c= the carrier of K by FINSEQ_1:def_4;
 0 + 1 <= n + 1 by NAT_1:13;
then A8: n + 1 in dom f by A6, FINSEQ_3:25;
then  f . (n + 1) in rng f by FUNCT_1:def_3;
then reconsider a = f . (n + 1) as Element of K by A7;
 rng f = rng g by A5, CLASSES1:75;
then  a in rng g by A8, FUNCT_1:def_3;
then consider m being Nat such that
A9: m in dom g and
A10: g . m = a by FINSEQ_2:10;
A11: g = (g | m) ^ (g /^ m) by RFINSEQ:8;
set gg = g /^ m;
set gm = g | m;
A12: 1 <= m by A9, FINSEQ_3:25;
then  max (0,(m - 1)) = m - 1 by FINSEQ_2:4;
then reconsider m1 = m - 1 as Element of NAT by FINSEQ_2:5;
 m in NAT by ORDINAL1:def_12;
then  m in Seg m by A12;
then A13: (g | m) . m = a by A9, A10, RFINSEQ:6;
A14: m = m1 + 1 ;
then  m1 <= m by NAT_1:11;
then A15: Seg m1 c= Seg m by FINSEQ_1:5;
 m <= len g by A9, FINSEQ_3:25;
then  len (g | m) = m by FINSEQ_1:59;
then A16: g | m = ((g | m) | m1) ^ <*a*> by A14, A13, RFINSEQ:7;
set fn = f | n1;
A17: f = (f | n1) ^ <*a*> by A6, RFINSEQ:7;
A18: (g | m) | m1 = g | ((Seg m) /\ (Seg m1)) by RELAT_1:71
.= g | m1 by A15, XBOOLE_1:28 ;
now__::_thesis:_for_x_being_set_holds_card_(Coim_((f_|_n1),x))_=_card_(Coim_(((g_|_m1)_^_(g_/^_m)),x))
let x be set ; ::_thesis: card (Coim ((f | n1),x)) = card (Coim (((g | m1) ^ (g /^ m)),x))
 card (Coim (f,x)) = card (Coim (g,x)) by A5, CLASSES1:def_9;
then (card ((f | n1) " {x})) + (card (<*a*> " {x})) = card ((((g | m1) ^ <*a*>) ^ (g /^ m)) " {x}) by A11, A16, A18, A17, FINSEQ_3:57
.= (card (((g | m1) ^ <*a*>) " {x})) + (card ((g /^ m) " {x})) by FINSEQ_3:57
.= ((card ((g | m1) " {x})) + (card (<*a*> " {x}))) + (card ((g /^ m) " {x})) by FINSEQ_3:57
.= ((card ((g | m1) " {x})) + (card ((g /^ m) " {x}))) + (card (<*a*> " {x}))
.= (card (((g | m1) ^ (g /^ m)) " {x})) + (card (<*a*> " {x})) by FINSEQ_3:57 ;
hence  card (Coim ((f | n1),x)) = card (Coim (((g | m1) ^ (g /^ m)),x)) ; ::_thesis: verum
end;
then A19: f | n1,(g | m1) ^ (g /^ m) are_fiberwise_equipotent by CLASSES1:def_9;
 len (f | n1) = n by A6, FINSEQ_1:59, NAT_1:11;
then  the multF of K $$ (f | n1) = the multF of K $$ ((g | m1) ^ (g /^ m)) by A4, A19;
hence  the multF of K $$ f = ( the multF of K $$ ((g | m1) ^ (g /^ m))) * ( the multF of K $$ <*a*>) by A17, FINSOP_1:5
.= (( the multF of K $$ (g | m1)) * ( the multF of K $$ (g /^ m))) * ( the multF of K $$ <*a*>) by FINSOP_1:5
.= (( the multF of K $$ (g | m1)) * ( the multF of K $$ <*a*>)) * ( the multF of K $$ (g /^ m)) by GROUP_1:def_3
.= ( the multF of K $$ (g | m)) * ( the multF of K $$ (g /^ m)) by A16, A18, FINSOP_1:5
.= the multF of K $$ g by A11, FINSOP_1:5 ;
::_thesis: verum
end;
A20: S1[ 0 ]
proof
let f, g be FinSequence of K; ::_thesis: ( f,g are_fiberwise_equipotent & len f = 0 implies the multF of K $$ f = the multF of K $$ g )
assume  ( f,g are_fiberwise_equipotent & len f = 0 ) ; ::_thesis: the multF of K $$ f = the multF of K $$ g
then A21: ( len g = 0 & f = <*> the carrier of K ) by RFINSEQ:3;
then  g = <*> the carrier of K ;
hence  the multF of K $$ f = the multF of K $$ g by A21; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A20, A3);
hence  the multF of K $$ R1 = the multF of K $$ R2 by A1, A2; ::_thesis: verum
end;

theorem Th32: :: MATRIX_7:32
for n being Element of NAT
for K being Field
for p being Element of Permutations n
for f, g being FinSequence of K st len f = n & g = f * p holds
f,g are_fiberwise_equipotent
proof
let n be Element of NAT ; ::_thesis: for K being Field
for p being Element of Permutations n
for f, g being FinSequence of K st len f = n & g = f * p holds
f,g are_fiberwise_equipotent
let K be Field; ::_thesis: for p being Element of Permutations n
for f, g being FinSequence of K st len f = n & g = f * p holds
f,g are_fiberwise_equipotent
let p be Element of Permutations n; ::_thesis: for f, g being FinSequence of K st len f = n & g = f * p holds
f,g are_fiberwise_equipotent
let f, g be FinSequence of K; ::_thesis: ( len f = n & g = f * p implies f,g are_fiberwise_equipotent )
assume that
A1: len f = n and
A2: g = f * p ; ::_thesis: f,g are_fiberwise_equipotent
reconsider fp = p as Function of (Seg n),(Seg n) by MATRIX_2:def_9;
A3: p is Permutation of (Seg n) by MATRIX_2:def_9;
then A4: rng p = Seg n by FUNCT_2:def_3;
 rng fp = Seg n by A3, FUNCT_2:def_3;
then  rng p c= dom f by A1, FINSEQ_1:def_3;
then A5: dom (f * p) = dom fp by RELAT_1:27;
 dom f = Seg n by A1, FINSEQ_1:def_3;
hence  f,g are_fiberwise_equipotent by A2, A5, A4, CLASSES1:77; ::_thesis: verum
end;

theorem :: MATRIX_7:33
for n being Element of NAT
for K being Field
for p being Element of Permutations n
for f, g being FinSequence of K st n >= 1 & len f = n & g = f * p holds
the multF of K $$ f = the multF of K $$ g by Th31, Th32;

theorem Th34: :: MATRIX_7:34
for n being Element of NAT
for K being Field
for p being Element of Permutations n
for f being FinSequence of K st n >= 1 & len f = n holds
f * p is FinSequence of K
proof
let n be Element of NAT ; ::_thesis: for K being Field
for p being Element of Permutations n
for f being FinSequence of K st n >= 1 & len f = n holds
f * p is FinSequence of K
let K be Field; ::_thesis: for p being Element of Permutations n
for f being FinSequence of K st n >= 1 & len f = n holds
f * p is FinSequence of K
let p be Element of Permutations n; ::_thesis: for f being FinSequence of K st n >= 1 & len f = n holds
f * p is FinSequence of K
let f be FinSequence of K; ::_thesis: ( n >= 1 & len f = n implies f * p is FinSequence of K )
assume that
A1: n >= 1 and
A2: len f = n ; ::_thesis: f * p is FinSequence of K
reconsider q = p as Function of (Seg n),(Seg n) by MATRIX_2:def_9;
 p is bijective Function of (Seg n),(Seg n) by MATRIX_2:def_9;
then  rng q = Seg n by FUNCT_2:def_3;
then  rng p c= dom f by A2, FINSEQ_1:def_3;
then  dom (f * p) = dom q by RELAT_1:27
.= Seg n by A1, FUNCT_2:def_1 ;
then reconsider h = f * p as FinSequence by FINSEQ_1:def_2;
 ( rng h c= rng f & rng f c= the carrier of K ) by FINSEQ_1:def_4, RELAT_1:26;
then  rng h c= the carrier of K by XBOOLE_1:1;
hence  f * p is FinSequence of K by FINSEQ_1:def_4; ::_thesis: verum
end;

theorem Th35: :: MATRIX_7:35
for n being Element of NAT
for K being Field
for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ")
proof
let n be Element of NAT ; ::_thesis: for K being Field
for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ")
let K be Field; ::_thesis: for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ")
let p be Element of Permutations n; ::_thesis: for A being Matrix of n,K st n >= 1 holds
Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ")
let A be Matrix of n,K; ::_thesis: ( n >= 1 implies Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ") )
set f = Path_matrix (p,A);
reconsider fp = p " as Function of (Seg n),(Seg n) by MATRIX_2:def_9;
reconsider fp0 = p as Function of (Seg n),(Seg n) by MATRIX_2:def_9;
assume A1: n >= 1 ; ::_thesis: Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ")
then A2: dom fp = Seg n by FUNCT_2:def_1;
A3: len (Path_matrix (p,A)) = n by MATRIX_3:def_7;
then reconsider m = (Path_matrix (p,A)) * (p ") as FinSequence of K by A1, Th34;
 p " is Permutation of (Seg n) by MATRIX_2:def_9;
then A4: rng fp = Seg n by FUNCT_2:def_3;
then  rng (p ") c= dom (Path_matrix (p,A)) by A3, FINSEQ_1:def_3;
then A5: dom ((Path_matrix (p,A)) * (p ")) = dom fp by RELAT_1:27;
A6: p is Permutation of (Seg n) by MATRIX_2:def_9;
A7: for i, j being Nat st i in dom m & j = (p ") . i holds
m . i = (A @) * (i,j)
proof
let i, j be Nat; ::_thesis: ( i in dom m & j = (p ") . i implies m . i = (A @) * (i,j) )
assume that
A8: i in dom m and
A9: j = (p ") . i ; ::_thesis: m . i = (A @) * (i,j)
A10: j in Seg n by A4, A5, A8, A9, FUNCT_1:def_3;
then A11: j in dom (Path_matrix (p,A)) by A3, FINSEQ_1:def_3;
 rng fp0 = Seg n by A6, FUNCT_2:def_3;
then  i = p . j by A5, A2, A8, A9, FUNCT_1:32;
then A12: (Path_matrix (p,A)) . j = A * (j,i) by A11, MATRIX_3:def_7;
A13: dom A = Seg (len A) by FINSEQ_1:def_3
.= Seg n by MATRIX_1:def_2 ;
 len A = n by MATRIX_1:def_2;
then  i in Seg (width A) by A1, A5, A2, A8, MATRIX_1:20;
then A14: [j,i] in Indices A by A10, A13, ZFMISC_1:def_2;
 ((Path_matrix (p,A)) * (p ")) . i = (Path_matrix (p,A)) . ((p ") . i) by A5, A8, FUNCT_1:13;
hence  m . i = (A @) * (i,j) by A9, A12, A14, MATRIX_1:def_6; ::_thesis: verum
end;
 len m = n by A5, A2, FINSEQ_1:def_3;
hence  Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ") by A7, MATRIX_3:def_7; ::_thesis: verum
end;

theorem Th36: :: MATRIX_7:36
for n being Element of NAT
for K being Field
for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
(Path_product (A @)) . (p ") = (Path_product A) . p
proof
let n be Element of NAT ; ::_thesis: for K being Field
for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
(Path_product (A @)) . (p ") = (Path_product A) . p
let K be Field; ::_thesis: for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
(Path_product (A @)) . (p ") = (Path_product A) . p
let p be Element of Permutations n; ::_thesis: for A being Matrix of n,K st n >= 1 holds
(Path_product (A @)) . (p ") = (Path_product A) . p
let A be Matrix of n,K; ::_thesis: ( n >= 1 implies (Path_product (A @)) . (p ") = (Path_product A) . p )
assume A1: n >= 1 ; ::_thesis: (Path_product (A @)) . (p ") = (Path_product A) . p
A2: len (Path_matrix (p,A)) = n by MATRIX_3:def_7;
then reconsider g = (Path_matrix (p,A)) * (p ") as FinSequence of K by A1, Th34;
(Path_product (A @)) . (p ") = - (( the multF of K $$ (Path_matrix ((p "),(A @)))),(p ")) by MATRIX_3:def_8
.= - (( the multF of K $$ g),(p ")) by A1, Th35
.= - (( the multF of K $$ g),p) by A1, Th29
.= - (( the multF of K $$ (Path_matrix (p,A))),p) by A2, Th31, Th32 ;
hence  (Path_product (A @)) . (p ") = (Path_product A) . p by MATRIX_3:def_8; ::_thesis: verum
end;

theorem :: MATRIX_7:37
for n being Element of NAT
for K being Field
for A being Matrix of n,K st n >= 1 holds
Det A = Det (A @)
proof
let n be Element of NAT ; ::_thesis: for K being Field
for A being Matrix of n,K st n >= 1 holds
Det A = Det (A @)
let K be Field; ::_thesis: for A being Matrix of n,K st n >= 1 holds
Det A = Det (A @)
let A be Matrix of n,K; ::_thesis: ( n >= 1 implies Det A = Det (A @) )
set f = Path_product A;
set f2 = Path_product (A @);
set F = the addF of K;
set Y = the carrier of K;
set X = Permutations n;
set B = FinOmega (Permutations n);
set I = the addF of K $$ ((FinOmega (Permutations n)),(Path_product (A @)));
A1: Det A = the addF of K $$ ((FinOmega (Permutations n)),(Path_product A)) by MATRIX_3:def_9;
A2: FinOmega (Permutations n) = Permutations n by MATRIX_2:26, MATRIX_2:def_14;
A3:  {  (p ") where p is Permutation of (Seg n) : p in FinOmega (Permutations n)  }  c= FinOmega (Permutations n)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  (p ") where p is Permutation of (Seg n) : p in FinOmega (Permutations n)  }  or z in FinOmega (Permutations n) )
assume  z in  {  (p ") where p is Permutation of (Seg n) : p in FinOmega (Permutations n)  }  ; ::_thesis: z in FinOmega (Permutations n)
then  ex p being Permutation of (Seg n) st
( z = p " & p in FinOmega (Permutations n) ) ;
hence  z in FinOmega (Permutations n) by A2, MATRIX_2:def_9; ::_thesis: verum
end;
A4: FinOmega (Permutations n) c=  {  (p ") where p is Permutation of (Seg n) : p in FinOmega (Permutations n)  }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in FinOmega (Permutations n) or z in  {  (p ") where p is Permutation of (Seg n) : p in FinOmega (Permutations n)  }  )
assume  z in FinOmega (Permutations n) ; ::_thesis: z in  {  (p ") where p is Permutation of (Seg n) : p in FinOmega (Permutations n)  }
then reconsider q2 = z as Permutation of (Seg n) by A2, MATRIX_2:def_9;
set q3 = q2 " ;
 ( (q2 ") " = q2 & q2 " in FinOmega (Permutations n) ) by A2, FUNCT_1:43, MATRIX_2:def_9;
hence  z in  {  (p ") where p is Permutation of (Seg n) : p in FinOmega (Permutations n)  }  ; ::_thesis: verum
end;
A5: ( FinOmega (Permutations n) <> {} or the addF of K is having_a_unity ) by MATRIX_2:26, MATRIX_2:def_14;
then consider G0 being Function of (Fin (Permutations n)), the carrier of K such that
A6: the addF of K $$ ((FinOmega (Permutations n)),(Path_product (A @))) = G0 . (FinOmega (Permutations n)) and
A7: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G0 . {} = e and
A8: for x being Element of Permutations n holds G0 . {x} = (Path_product (A @)) . x and
A9: for B9 being Element of Fin (Permutations n) st B9 c= FinOmega (Permutations n) & B9 <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (A @)) . x)) by SETWISEO:def_3;
deffunc H1( set ) ->  set = G0 .  {  (p ") where p is Permutation of (Seg n) : p in $1  }  ;
A10: for x2 being set st x2 in Fin (Permutations n) holds
H1(x2) in the carrier of K
proof
let x2 be set ; ::_thesis: ( x2 in Fin (Permutations n) implies H1(x2) in the carrier of K )
assume  x2 in Fin (Permutations n) ; ::_thesis: H1(x2) in the carrier of K
  {  (p ") where p is Permutation of (Seg n) : p in x2  }  c= Permutations n
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in  {  (p ") where p is Permutation of (Seg n) : p in x2  }  or r in Permutations n )
assume  r in  {  (p ") where p is Permutation of (Seg n) : p in x2  }  ; ::_thesis: r in Permutations n
then  ex p being Permutation of (Seg n) st
( r = p " & p in x2 ) ;
hence  r in Permutations n by MATRIX_2:def_9; ::_thesis: verum
end;
then   {  (p ") where p is Permutation of (Seg n) : p in x2  }  is Finite_Subset of (Permutations n) by FINSUB_1:18, MATRIX_2:26;
hence  H1(x2) in the carrier of K by FUNCT_2:5; ::_thesis: verum
end;
consider G1 being Function of (Fin (Permutations n)), the carrier of K such that
A11: for x5 being set st x5 in Fin (Permutations n) holds
G1 . x5 = H1(x5) from FUNCT_2:sch_2(A10);
assume A12: n >= 1 ; ::_thesis: Det A = Det (A @)
A13: for x being Element of Permutations n holds G1 . {x} = (Path_product A) . x
proof
let x be Element of Permutations n; ::_thesis: G1 . {x} = (Path_product A) . x
reconsider B4 = {.x.} as Element of Fin (Permutations n) ;
reconsider q = x as Permutation of (Seg n) by MATRIX_2:def_9;
A14: q " is Element of Permutations n by MATRIX_2:def_9;
A15:  {  (p ") where p is Permutation of (Seg n) : p in B4  }  c= {(q ")}
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  (p ") where p is Permutation of (Seg n) : p in B4  }  or z in {(q ")} )
assume  z in  {  (p ") where p is Permutation of (Seg n) : p in B4  }  ; ::_thesis: z in {(q ")}
then consider p being Permutation of (Seg n) such that
A16: z = p " and
A17: p in B4 ;
 p = x by A17, TARSKI:def_1;
hence  z in {(q ")} by A16, TARSKI:def_1; ::_thesis: verum
end;
 {(q ")} c=  {  (p ") where p is Permutation of (Seg n) : p in B4  }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {(q ")} or z in  {  (p ") where p is Permutation of (Seg n) : p in B4  }  )
assume  z in {(q ")} ; ::_thesis: z in  {  (p ") where p is Permutation of (Seg n) : p in B4  }
then  ( q in B4 & z = q " ) by TARSKI:def_1;
hence  z in  {  (p ") where p is Permutation of (Seg n) : p in B4  }  ; ::_thesis: verum
end;
then   {  (p ") where p is Permutation of (Seg n) : p in B4  }  = {(q ")} by A15, XBOOLE_0:def_10;
then G1 . B4 = G0 . {(q ")} by A11
.= (Path_product (A @)) . (q ") by A8, A14
.= (Path_product A) . q by A12, Th36 ;
hence  G1 . {x} = (Path_product A) . x ; ::_thesis: verum
end;
A18: for B9 being Element of Fin (Permutations n) st B9 c= FinOmega (Permutations n) & B9 <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G1 . (B9 \/ {x}) = the addF of K . ((G1 . B9),((Path_product A) . x))
proof
let B9 be Element of Fin (Permutations n); ::_thesis: ( B9 c= FinOmega (Permutations n) & B9 <> {} implies for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G1 . (B9 \/ {x}) = the addF of K . ((G1 . B9),((Path_product A) . x)) )
assume that
A19: B9 c= FinOmega (Permutations n) and
A20: B9 <> {} ; ::_thesis: for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G1 . (B9 \/ {x}) = the addF of K . ((G1 . B9),((Path_product A) . x))
thus  for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G1 . (B9 \/ {x}) = the addF of K . ((G1 . B9),((Path_product A) . x)) ::_thesis: verum
proof
  {  (p ") where p is Permutation of (Seg n) : p in B9  }  c= Permutations n
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in  {  (p ") where p is Permutation of (Seg n) : p in B9  }  or v in Permutations n )
assume  v in  {  (p ") where p is Permutation of (Seg n) : p in B9  }  ; ::_thesis: v in Permutations n
then  ex p being Permutation of (Seg n) st
( p " = v & p in B9 ) ;
hence  v in Permutations n by MATRIX_2:def_9; ::_thesis: verum
end;
then reconsider B2 =  {  (p ") where p is Permutation of (Seg n) : p in B9  }  as Element of Fin (Permutations n) by FINSUB_1:18, MATRIX_2:26;
set d = the Element of B9;
let x be Element of Permutations n; ::_thesis: ( x in (FinOmega (Permutations n)) \ B9 implies G1 . (B9 \/ {x}) = the addF of K . ((G1 . B9),((Path_product A) . x)) )
reconsider px = x as Permutation of (Seg n) by MATRIX_2:def_9;
reconsider y = px " as Element of Permutations n by MATRIX_2:def_9;
A21: B2 \/ {y} c=  {  (p ") where p is Permutation of (Seg n) : p in B9 \/ {x}  }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in B2 \/ {y} or z in  {  (p ") where p is Permutation of (Seg n) : p in B9 \/ {x}  }  )
assume  z in B2 \/ {y} ; ::_thesis: z in  {  (p ") where p is Permutation of (Seg n) : p in B9 \/ {x}  }
then A22: ( z in B2 or z in {y} ) by XBOOLE_0:def_3;
now__::_thesis:_(_(_z_in_B2_&_z_in__{__(p_")_where_p_is_Permutation_of_(Seg_n)_:_p_in_B9_\/_{x}__}__)_or_(_z_=_y_&_z_in__{__(p_")_where_p_is_Permutation_of_(Seg_n)_:_p_in_B9_\/_{x}__}__)_)
percases ( z in B2 or z = y ) by A22, TARSKI:def_1;
case z in B2 ; ::_thesis: z in  {  (p ") where p is Permutation of (Seg n) : p in B9 \/ {x}  }
then consider p being Permutation of (Seg n) such that
A23: z = p " and
A24: p in B9 ;
 p in B9 \/ {x} by A24, XBOOLE_0:def_3;
hence  z in  {  (p ") where p is Permutation of (Seg n) : p in B9 \/ {x}  }  by A23; ::_thesis: verum
end;
caseA25: z = y ; ::_thesis: z in  {  (p ") where p is Permutation of (Seg n) : p in B9 \/ {x}  }
 px in {x} by TARSKI:def_1;
then  px in B9 \/ {x} by XBOOLE_0:def_3;
hence  z in  {  (p ") where p is Permutation of (Seg n) : p in B9 \/ {x}  }  by A25; ::_thesis: verum
end;
end;
end;
hence  z in  {  (p ") where p is Permutation of (Seg n) : p in B9 \/ {x}  }  ; ::_thesis: verum
end;
A26: B2 c= FinOmega (Permutations n)
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in B2 or u in FinOmega (Permutations n) )
assume  u in B2 ; ::_thesis: u in FinOmega (Permutations n)
then  ex p being Permutation of (Seg n) st
( p " = u & p in B9 ) ;
hence  u in FinOmega (Permutations n) by A2, MATRIX_2:def_9; ::_thesis: verum
end;
assume  x in (FinOmega (Permutations n)) \ B9 ; ::_thesis: G1 . (B9 \/ {x}) = the addF of K . ((G1 . B9),((Path_product A) . x))
then A27: not x in B9 by XBOOLE_0:def_5;
now__::_thesis:_not_y_in_B2
assume  y in B2 ; ::_thesis: contradiction
then consider pp being Permutation of (Seg n) such that
A28: y = pp " and
A29: pp in B9 ;
 px = (pp ") " by A28, FUNCT_1:43;
hence  contradiction by A27, A29, FUNCT_1:43; ::_thesis: verum
end;
then A30: y in (FinOmega (Permutations n)) \ B2 by A2, XBOOLE_0:def_5;
 the Element of B9 in FinOmega (Permutations n) by A19, A20, TARSKI:def_3;
then reconsider pd = the Element of B9 as Permutation of (Seg n) by A2, MATRIX_2:def_9;
A31: pd " in B2 by A20;
A32: ( G1 . (B9 \/ {.x.}) = G0 .  {  (p ") where p is Permutation of (Seg n) : p in B9 \/ {x}  }  & G0 . B2 = G1 . B9 ) by A11;
  {  (p ") where p is Permutation of (Seg n) : p in B9 \/ {x}  }  c= B2 \/ {y}
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  (p ") where p is Permutation of (Seg n) : p in B9 \/ {x}  }  or z in B2 \/ {y} )
assume  z in  {  (p ") where p is Permutation of (Seg n) : p in B9 \/ {x}  }  ; ::_thesis: z in B2 \/ {y}
then consider p being Permutation of (Seg n) such that
A33: z = p " and
A34: p in B9 \/ {x} ;
now__::_thesis:_(_(_p_in_B9_&_(_z_in_B2_or_z_in_{y}_)_)_or_(_p_in_{x}_&_(_z_in_B2_or_z_in_{y}_)_)_)
percases ( p in B9 or p in {x} ) by A34, XBOOLE_0:def_3;
case p in B9 ; ::_thesis: ( z in B2 or z in {y} )
hence  ( z in B2 or z in {y} ) by A33; ::_thesis: verum
end;
case p in {x} ; ::_thesis: ( z in B2 or z in {y} )
then  p = x by TARSKI:def_1;
hence  ( z in B2 or z in {y} ) by A33, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  z in B2 \/ {y} by XBOOLE_0:def_3; ::_thesis: verum
end;
then  B2 \/ {y} =  {  (p ") where p is Permutation of (Seg n) : p in B9 \/ {x}  }  by A21, XBOOLE_0:def_10;
then  G0 .  {  (p ") where p is Permutation of (Seg n) : p in B9 \/ {x}  }  = the addF of K . ((G0 . B2),((Path_product (A @)) . y)) by A9, A26, A31, A30;
hence  G1 . (B9 \/ {x}) = the addF of K . ((G1 . B9),((Path_product A) . x)) by A12, A32, Th36; ::_thesis: verum
end;
end;
A35: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G1 . {} = e
proof
 {} is Subset of (Permutations n) by SUBSET_1:1;
then reconsider B3 = {} as Element of Fin (Permutations n) by FINSUB_1:18, MATRIX_2:26;
let e be Element of the carrier of K; ::_thesis: ( e is_a_unity_wrt the addF of K implies G1 . {} = e )
  {  (p ") where p is Permutation of (Seg n) : p in B3  }  c= {}
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in  {  (p ") where p is Permutation of (Seg n) : p in B3  }  or s in {} )
assume  s in  {  (p ") where p is Permutation of (Seg n) : p in B3  }  ; ::_thesis: s in {}
then  ex p being Permutation of (Seg n) st
( s = p " & p in B3 ) ;
hence  s in {} ; ::_thesis: verum
end;
then A36:  {  (p ") where p is Permutation of (Seg n) : p in B3  }  = {} ;
assume  e is_a_unity_wrt the addF of K ; ::_thesis: G1 . {} = e
then  G0 .  {  (p ") where p is Permutation of (Seg n) : p in B3  }  = e by A7, A36;
hence  G1 . {} = e by A11; ::_thesis: verum
end;
 G1 . (FinOmega (Permutations n)) = G0 .  {  (p ") where p is Permutation of (Seg n) : p in FinOmega (Permutations n)  }  by A11;
then  the addF of K $$ ((FinOmega (Permutations n)),(Path_product (A @))) = G1 . (FinOmega (Permutations n)) by A6, A3, A4, XBOOLE_0:def_10;
then  the addF of K $$ ((FinOmega (Permutations n)),(Path_product A)) = the addF of K $$ ((FinOmega (Permutations n)),(Path_product (A @))) by A5, A35, A13, A18, SETWISEO:def_3;
hence  Det A = Det (A @) by A1, MATRIX_3:def_9; ::_thesis: verum
end;