let K be Ring; :: thesis: for n being Nat st n >= 1 holds
Det (1. (K,n)) = 1_ K
let n be Nat; :: thesis: ( n >= 1 implies Det (1. (K,n)) = 1_ K )
assume A1: n >= 1 ; :: thesis: Det (1. (K,n)) = 1_ K
deffunc H₁( object ) -> 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 object st x in Permutations n holds
H₁(x) in the carrier of K ;
ex f2 being Function of (Permutations n), the carrier of K st
for x being object st x in Permutations n holds
f2 . x = H₁(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 object st x in Permutations n holds
f2 . x = H₁(x) ;
A4: id (Seg n) is even by MATRIX_1:16;
A5: for x being object st x in dom (Path_product (1. (K,n))) holds
(Path_product (1. (K,n))) . x = f2 . x

proof

let x be object ; :: 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 S₁[ 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 Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A7: ((k + 1) + 1) |-> (1_ K) = ((k + 1) |-> (1_ K)) ^ <*(1_ K)*> by FINSEQ_2:60;
assume S₁[k] ; :: thesis: S₁[k + 1]
then the multF of K $$ (((k + 1) + 1) |-> (1_ K)) = (1_ K) * (1_ K) by A7, FINSOP_1:4
.= 1_ K ;
hence S₁[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 ) )

per cases ( 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_1:def 16; :: thesis: verum

end;

case not p is even ; :: thesis: - ((0. K),p) = 0. K

then - ((0. K),p) = - (0. K) by MATRIX_1:def 16
.= 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: S₁[ 0 ] by FINSOP_1:11;
for k being Nat holds S₁[k] from NAT_1:sch 2(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) ) )

per cases ( p = idseq n or p <> idseq n ) ;

case A12: 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_0: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 3; :: thesis: verum

end;

len (Permutations n) = n by MATRIX_1:9;
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_1:def 16;
f2 . p = H₁(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;

case A20: 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 S₂[ 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 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 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_1:9;
then dom p = dom (idseq n) by RELAT_1:45;
then consider i0 being object 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 Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A30: S₂[k] ; :: thesis: S₂[k + 1]

now :: thesis: ( ( k + 1 < n & S₂[k + 1] ) or ( k + 1 >= n & S₂[k + 1] ) )

per cases ( k + 1 < n or k + 1 >= n ) ;

case A31: k + 1 < n ; :: thesis: S₂[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 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 S₃[ object , object ] means ( ( $1 in Seg (k + 1) implies $2 = p3 . $1 ) & ( not $1 in Seg (k + 1) implies $2 = 0. K ) );
A35: for x being object st x in NAT holds
ex y being object st
( y in the carrier of K & S₃[x,y] )

proof

let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in the carrier of K & S₃[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in the carrier of K & S₃[x,y] )

now :: thesis: ( ( x in Seg (k + 1) & ex y being object st
( y in the carrier of K & S₃[x,y] ) ) or ( not x in Seg (k + 1) & ex y being object st
( y in the carrier of K & S₃[x,y] ) ) )

per cases ( x in Seg (k + 1) or not x in Seg (k + 1) ) ;

case A36: x in Seg (k + 1) ; :: thesis: ex y being object st
( y in the carrier of K & S₃[x,y] )

then reconsider nx = x as 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 object st
( y in the carrier of K & S₃[x,y] ) by A36; :: thesis: verum

end;

case not x in Seg (k + 1) ; :: thesis: ex y being object st
( y in the carrier of K & S₃[x,y] )

hence ex y being object st
( y in the carrier of K & S₃[x,y] ) ; :: thesis: verum

end;

end;

end;

hence ex y being object st
( y in the carrier of K & S₃[x,y] ) ; :: thesis: verum

end;

ex f6 being sequence of the carrier of K st
for x being object st x in NAT holds
S₃[x,f6 . x] from FUNCT_2:sch 1(A35);
then consider f6 being sequence of the carrier of K such that
A38: for x being object st x in NAT holds
S₃[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 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 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))) ) )

per cases ( n3 < k + 1 or n3 >= k + 1 ) ;

case A44: 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;

case A47: 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 ;
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 S₂[k + 1] by A39, A40; :: thesis: verum

end;

case k + 1 >= n ; :: thesis: S₂[k + 1]

hence S₂[k + 1] ; :: thesis: verum

end;

end;

end;

hence S₂[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 = H₁(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: S₂[ 0 ] by A23;
for k being Nat holds S₂[k] from NAT_1:sch 2(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 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 S₃[ 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 S₃[x3,y3]

proof

let x3 be Element of A; :: thesis: ex y3 being Element of K st S₃[x3,y3]

now :: thesis: ( ( x3 in Seg n & ex y3 being Element of K st S₃[x3,y3] ) or ( not x3 in Seg n & ex y3 being Element of K st S₃[x3,y3] ) )

per cases ( x3 in Seg n or not x3 in Seg n ) ;

case A61: x3 in Seg n ; :: thesis: ex y3 being Element of K st S₃[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 S₃[x3,y3] by A61; :: thesis: verum

end;

case not x3 in Seg n ; :: thesis: ex y3 being Element of K st S₃[x3,y3]

hence ex y3 being Element of K st S₃[x3,y3] ; :: thesis: verum

end;

end;

end;

hence ex y3 being Element of K st S₃[x3,y3] ; :: thesis: verum

end;

ex f4 being Function of A, the carrier of K st
for x2 being Element of A holds S₃[x2,f4 . x2] from FUNCT_2:sch 3(A60);
then consider f4 being sequence of 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_1:def 12;
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_0: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 S₄[ Nat] means f4 . (i0 + $1) = 0. K;
A67: 0 < i0 by A24, A26, FINSEQ_1:1;
A68: for k being Nat st S₄[k] holds
S₄[k + 1]

proof

let k be Nat; :: thesis: ( S₄[k] implies S₄[k + 1] )
A69: 1 <= 1 + (i0 + k) by NAT_1:12;
assume A70: S₄[k] ; :: thesis: S₄[k + 1]

now :: thesis: ( ( (i0 + k) + 1 <= n & S₄[k + 1] ) or ( (i0 + k) + 1 > n & S₄[k + 1] ) )

per cases ( (i0 + k) + 1 <= n or (i0 + k) + 1 > n ) ;

case A71: (i0 + k) + 1 <= n ; :: thesis: S₄[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 ;
hence S₄[k + 1] ; :: thesis: verum

end;

case (i0 + k) + 1 > n ; :: thesis: S₄[k + 1]

then not i0 + (k + 1) in Seg n by FINSEQ_1:1;
hence S₄[k + 1] by A62; :: thesis: verum

end;

end;

end;

hence S₄[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 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 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 & S₄[ 0 ] ) or ( i0 > 1 & S₄[ 0 ] ) )

per cases ( i0 <= 1 or i0 > 1 ) ;

case i0 <= 1 ; :: thesis: S₄[ 0 ]

then i0 = 1 by A83, XXREAL_0:1;
hence S₄[ 0 ] by A28, A66, A64, A75, MATRIX_1:def 3; :: thesis: verum

end;

case A84: i0 > 1 ; :: thesis: S₄[ 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 3
.= 0. K ;
hence S₄[ 0 ] ; :: thesis: verum

end;

end;

end;

then A88: S₄[ 0 ] ;
for k being Nat holds S₄[k] from NAT_1:sch 2(A88, A68);
then S₄[n -' i0] ;
then f4 . (i0 + (n -' i0)) = 0. K ;
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 H₂( set ) -> object = IFIN ((idseq n),$1,(1_ K),(0. K));
set F = the addF of K;
set f = Path_product (1. (K,n));
set B = In ((Permutations n),(Fin (Permutations n)));
A89: for x being set st x in Fin (Permutations n) holds
H₂(x) in the carrier of K

proof

let x be set ; :: thesis: ( x in Fin (Permutations n) implies H₂(x) in the carrier of K )
assume x in Fin (Permutations n) ; :: thesis: H₂(x) in the carrier of K

now :: thesis: ( ( idseq n in x & H₂(x) in the carrier of K ) or ( not idseq n in x & H₂(x) in the carrier of K ) )

per cases ( idseq n in x or not idseq n in x ) ;

case idseq n in x ; :: thesis: H₂(x) in the carrier of K

then H₂(x) = 1_ K by Def1;
hence H₂(x) in the carrier of K ; :: thesis: verum

end;

case not idseq n in x ; :: thesis: H₂(x) in the carrier of K

then H₂(x) = 0. K by Def1;
hence H₂(x) in the carrier of K ; :: thesis: verum

end;

end;

end;

hence H₂(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 = H₂(x) from FUNCT_2:sch 11(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 = H₂(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= In ((Permutations n),(Fin (Permutations n))) & B9 <> {} holds
for x being Element of Permutations n st x in (In ((Permutations n),(Fin (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= In ((Permutations n),(Fin (Permutations n))) & B9 <> {} implies for x being Element of Permutations n st x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) )
assume that
B9 c= In ((Permutations n),(Fin (Permutations n))) and
B9 <> {} ; :: thesis: for x being Element of Permutations n st x in (In ((Permutations n),(Fin (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 (In ((Permutations n),(Fin (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 (In ((Permutations n),(Fin (Permutations n)))) \ B9 implies G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) )
assume A94: x in (In ((Permutations n),(Fin (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 = H₁(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 ) )

per cases ( idseq n in B9 or idseq n = x ) by A106, TARSKI:def 1;

case A107: 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 = H₁(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;

case A109: idseq n = x ; :: thesis: the addF of K . ((G0 . B9),((Path_product (1. (K,n))) . x)) = 1_ K

(Path_product (1. (K,n))) . x = H₁(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 ) )

per cases ( x = idseq n or x <> idseq n ) ;

case A112: 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 = H₁(x) by A3
.= 1_ K by A112, FUNCOP_1:def 8 ;
hence G0 . {.x.} = f2 . x by A90, A113; :: thesis: verum

end;

case A114: 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 = H₁(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 In ((Permutations n),(Fin (Permutations n))) implies G0 . (In ((Permutations n),(Fin (Permutations n)))) = 1_ K )

assume A120: idseq n in In ((Permutations n),(Fin (Permutations n))) ; :: thesis: G0 . (In ((Permutations n),(Fin (Permutations n)))) = 1_ K
thus G0 . (In ((Permutations n),(Fin (Permutations n)))) = IFIN ((idseq n),(In ((Permutations n),(Fin (Permutations n)))),(1_ K),(0. K)) by A90
.= 1_ K by A120, Def1 ; :: thesis: verum

end;

S: idseq n is Element of (Group_of_Perm n) by MATRIX_1:11;
Permutations n in Fin (Permutations n) by FINSUB_1:def 5;
then ( In ((Permutations n),(Fin (Permutations n))) = Permutations n & idseq n in the carrier of (Group_of_Perm n) ) by S, SUBSET_1:def 8;
then the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product (1. (K,n)))) = 1_ K by A119, A116, A111, A93, MATRIX_1:def 13, SETWISEO:def 3;
hence Det (1. (K,n)) = 1_ K by MATRIX_3:def 9; :: thesis: verum