let n be Nat; :: thesis:
let p1 be Element of Permutations (n + 1); :: thesis:
let K be Field; :: thesis:
let a be Element of K; :: thesis:
set n1 = n + 1;
let i, j be Nat; :: thesis:
assume that
A1: i in Seg (n + 1) and
A2: p1 . i = j ; :: thesis:
A3: p1 is Permutation of (Seg (n + 1)) by MATRIX_1:def 12;
then A4: rng p1 = Seg (n + 1) by FUNCT_2:def 3;
dom p1 = Seg (n + 1) by A3, FUNCT_2:52;
then A5: j in Seg (n + 1) by A1, A2, A4, FUNCT_1:def 3;
set R = Rem (p1,i);

per cases by NAT_1:23;

suppose A6: n = 0 ; :: thesis:

then Rem (p1,i) is even by Th11;
then A7: - (a,(Rem (p1,i))) = a by MATRIX_1:def 16;
A8: 1 + 1 = 2 * 1 ;
p1 is even by A6, Th11;
then A9: - (a,p1) = a by MATRIX_1:def 16;
A10: j = 1 by A5, A6, FINSEQ_1:2, TARSKI:def 1;
i = 1 by A1, A6, FINSEQ_1:2, TARSKI:def 1;
then (power K) . ((- (1_ K)),(i + j)) = 1_ K by A10, A8, HURWITZ:4;
hence - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i)))) by A9, A7; :: thesis:

end;

suppose A11: n = 1 ; :: thesis:

then A12: p1 is Permutation of (Seg 2) by MATRIX_1:def 12;

per cases by A12, MATRIX_7:1;

suppose A13: p1 = <*1,2*> ; :: thesis:

( i = 1 or i = 2 ) by A1, A11, FINSEQ_1:2, TARSKI:def 2;
then ( ( i = 1 & p1 . i = 1 ) or ( i = 2 & p1 . i = 2 ) ) by A13;
then ( i + j = 2 * 1 or i + j = 2 * 2 ) by A2;
then A14: (power K) . ((- (1_ K)),(i + j)) = 1_ K by HURWITZ:4;
A15: len (Permutations 2) = 2 by MATRIX_1:9;
Rem (p1,i) is even by A11, Th11;
then A16: - (a,(Rem (p1,i))) = a by MATRIX_1:def 16;
id (Seg 2) is even by MATRIX_1:16;
then - (a,p1) = a by A11, A13, A15, FINSEQ_2:52, MATRIX_1:def 16;
hence - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i)))) by A14, A16; :: thesis:

end;

suppose A17: p1 = <*2,1*> ; :: thesis:

len (Permutations 2) = 2 by MATRIX_1:9;
then - (a,p1) = - a by A11, A17, MATRIX_1:def 16, MATRIX_9:12;
then A18: - (a,p1) = - ((1_ K) * a) ;
( i = 1 or i = 2 ) by A1, A11, FINSEQ_1:2, TARSKI:def 2;
then i + j = (2 * 1) + 1 by A2, A17;
then A19: (power K) . ((- (1_ K)),(i + j)) = - (1_ K) by HURWITZ:4;
Rem (p1,i) is even by A11, Th11;
then - (a,(Rem (p1,i))) = a by MATRIX_1:def 16;
hence - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i)))) by A19, A18, VECTSP_1:8; :: thesis:

end;

suppose A20: n >= 2 ; :: thesis:

then reconsider n2 = n - 2 as Element of NAT by NAT_1:21;

per cases ;

suppose A21: not K is Fanoian ; :: thesis:

A22: now :: thesis:

per cases ) mod 2 = 0 or (i + j) mod 2 = 1 ) by NAT_D:12;

suppose (i + j) mod 2 = 0 ; :: thesis:

then consider t being Nat such that
A23: i + j = (2 * t) + 0 and
0 < 2 by NAT_D:def 2;
t is Element of NAT by ORDINAL1:def 12;
hence (power K) . ((- (1_ K)),(i + j)) = 1_ K by A23, HURWITZ:4; :: thesis:

end;

suppose (i + j) mod 2 = 1 ; :: thesis:

then consider t being Nat such that
A24: i + j = (2 * t) + 1 and
1 < 2 by NAT_D:def 2;
A25: 1_ K = - (1_ K) by A21, MATRIX11:22;
t is Element of NAT by ORDINAL1:def 12;
hence (power K) . ((- (1_ K)),(i + j)) = 1_ K by A24, A25, HURWITZ:4; :: thesis:

end;

A26: ( - (a,p1) = a or - (a,p1) = - a ) by MATRIX_1:def 16;
- (1_ K) = 1_ K by A21, MATRIX11:22;
then A27: - (a * (1_ K)) = a * (1_ K) by VECTSP_1:9;
( - (a,(Rem (p1,i))) = a or - (a,(Rem (p1,i))) = - a ) by MATRIX_1:def 16;
then - (a,(Rem (p1,i))) = a by A27;
hence - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i)))) by A22, A26, A27; :: thesis:

end;

suppose A29: K is Fanoian ; :: thesis:

set mm = the multF of K;
reconsider n1 = n2 + 1 as Element of NAT ;
set P1 = Permutations (n1 + 2);
reconsider Q1 = p1 as Element of Permutations (n1 + 2) ;
set SS1 = 2Set (Seg (n1 + 2));
consider X being Element of Fin (2Set (Seg (n1 + 2))) such that
A30: X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n1 + 2)) } and
A31: the multF of K $$ (X,(Part_sgn (Q1,K))) = (power K) . ((- (1_ K)),(i + j)) by A1, A2, A29, Th9;
set PQ1 = Part_sgn (Q1,K);
set SS2 = 2Set (Seg (n2 + 2));
reconsider Q19 = Q1 as Permutation of (Seg (n1 + 2)) by MATRIX_1:def 12;
set P2 = Permutations (n2 + 2);
reconsider Q = Rem (p1,i) as Element of Permutations (n2 + 2) ;
reconsider Q9 = Q as Permutation of (Seg (n2 + 2)) by MATRIX_1:def 12;
set PQ = Part_sgn (Q,K);
2Set (Seg (n1 + 2)) in Fin (2Set (Seg (n1 + 2))) by FINSUB_1:def 5;
then A32: In ((2Set (Seg (n1 + 2))),(Fin (2Set (Seg (n1 + 2))))) = 2Set (Seg (n1 + 2)) by SUBSET_1:def 8;
reconsider SSX = (2Set (Seg (n1 + 2))) \ X as Element of Fin (2Set (Seg (n1 + 2))) by FINSUB_1:def 5;
A33: X \/ SSX = (2Set (Seg (n1 + 2))) \/ X by XBOOLE_1:39;
X c= 2Set (Seg (n1 + 2)) by FINSUB_1:def 5;
then A34: X \/ SSX = 2Set (Seg (n1 + 2)) by A33, XBOOLE_1:12;
consider f being Function of (2Set (Seg (n2 + 2))),(2Set (Seg (n1 + 2))) such that
A35: rng f = (2Set (Seg (n1 + 2))) \ X and
A36: f is one-to-one and
A37: for k, m being Nat st k < m & {k,m} in 2Set (Seg (n2 + 2)) holds
( ( m < i & k < i implies f . {k,m} = {k,m} ) & ( m >= i & k < i implies f . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies f . {k,m} = {(k + 1),(m + 1)} ) ) by A1, A20, A30, Th10;
set Pf = (Part_sgn (Q1,K)) * f;
A38: dom ((Part_sgn (Q1,K)) * f) = 2Set (Seg (n2 + 2)) by FUNCT_2:def 1;
A39: dom Q19 = Seg (n1 + 2) by FUNCT_2:52;

A40: now :: thesis:

n <= n + 1 by NAT_1:11;
then A41: Seg (n2 + 2) c= Seg (n1 + 2) by FINSEQ_1:5;
let x be object ; :: thesis:
assume A42: x in 2Set (Seg (n2 + 2)) ; :: thesis:
consider k, m being Nat such that
A43: k in Seg (n2 + 2) and
A44: m in Seg (n2 + 2) and
A45: k < m and
A46: x = {k,m} by A42, MATRIX11:1;
reconsider k = k, m = m as Element of NAT by ORDINAL1:def 12;
dom Q9 = Seg (n2 + 2) by FUNCT_2:52;
then Q9 . k <> Q . m by A43, A44, A45, FUNCT_1:def 4;
then A47: ( Q . k > Q . m or Q . k < Q . m ) by XXREAL_0:1;
set m1 = m + 1;
set k1 = k + 1;
A48: (n2 + 2) + 1 = n1 + 2 ;
then A49: k + 1 in Seg (n1 + 2) by A43, FINSEQ_1:60;
A50: m + 1 in Seg (n1 + 2) by A44, A48, FINSEQ_1:60;

per cases ;

suppose A51: ( k < i & m < i ) ; :: thesis:

A52: ((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q1,K)) . (f . x) by A38, A42, FUNCT_1:12;
A53: f . x = x by A37, A42, A45, A46, A51;

per cases ;

suppose ( ( Q1 . k < j & Q1 . m < j ) or ( Q1 . k >= j & Q1 . m >= j ) ) ; :: thesis:

then ( ( Q . k = Q1 . k & Q . m = Q1 . m ) or ( Q . k = (Q1 . k) - 1 & Q . m = (Q1 . m) - 1 ) ) by A1, A2, A43, A44, A51, Def3;
then ( ( Q . k < Q . m & Q1 . k < Q1 . m ) or ( Q . k > Q . m & Q1 . k > Q1 . m ) ) by A47, XREAL_1:9;
then ( ( (Part_sgn (Q1,K)) . x = 1_ K & (Part_sgn (Q,K)) . x = 1_ K ) or ( (Part_sgn (Q1,K)) . x = - (1_ K) & (Part_sgn (Q,K)) . x = - (1_ K) ) ) by A43, A44, A45, A46, A41, MATRIX11:def 1;
hence ((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q,K)) . x by A38, A42, A53, FUNCT_1:12; :: thesis:

end;

suppose A54: ( Q1 . k < j & Q1 . m >= j ) ; :: thesis:

then Q . m = (Q1 . m) - 1 by A1, A2, A44, A51, Def3;
then A55: Q1 . m = (Q . m) + 1 ;
Q19 . m <> j by A1, A2, A39, A44, A41, A51, FUNCT_1:def 4;
then Q1 . m > j by A54, XXREAL_0:1;
then A56: Q . m >= j by A55, NAT_1:13;
Q1 . k < Q1 . m by A54, XXREAL_0:2;
then A57: (Part_sgn (Q1,K)) . x = 1_ K by A43, A44, A45, A46, A41, MATRIX11:def 1;
Q1 . k = Q . k by A1, A2, A43, A51, A54, Def3;
then Q . k < Q . m by A54, A56, XXREAL_0:2;
hence ((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q,K)) . x by A43, A44, A45, A46, A53, A52, A57, MATRIX11:def 1; :: thesis:

end;

suppose A58: ( Q1 . k >= j & Q1 . m < j ) ; :: thesis:

then Q . k = (Q1 . k) - 1 by A1, A2, A43, A51, Def3;
then A59: Q1 . k = (Q . k) + 1 ;
Q19 . k <> j by A1, A2, A39, A43, A41, A51, FUNCT_1:def 4;
then Q1 . k > j by A58, XXREAL_0:1;
then A60: Q . k >= j by A59, NAT_1:13;
Q1 . k > Q1 . m by A58, XXREAL_0:2;
then A61: (Part_sgn (Q1,K)) . x = - (1_ K) by A43, A44, A45, A46, A41, MATRIX11:def 1;
Q1 . m = Q . m by A1, A2, A44, A51, A58, Def3;
then Q . k > Q . m by A58, A60, XXREAL_0:2;
hence ((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q,K)) . x by A43, A44, A45, A46, A53, A52, A61, MATRIX11:def 1; :: thesis:

end;

suppose ( k >= i & m < i ) ; :: thesis:

hence ((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q,K)) . x by A45, XXREAL_0:2; :: thesis:

end;

suppose A62: ( k < i & m >= i ) ; :: thesis:

A63: ((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q1,K)) . (f . {k,m}) by A38, A42, A46, FUNCT_1:12;
A64: f . {k,m} = {k,(m + 1)} by A37, A42, A45, A46, A62;

per cases ;

suppose ( ( Q1 . k < j & Q1 . (m + 1) < j ) or ( Q1 . k >= j & Q1 . (m + 1) >= j ) ) ; :: thesis:

then ( ( Q . k = Q1 . k & Q . m = Q1 . (m + 1) ) or ( Q . k = (Q1 . k) - 1 & Q . m = (Q1 . (m + 1)) - 1 ) ) by A1, A2, A43, A44, A62, Def3;
then A65: ( ( Q . k < Q . m & Q1 . k < Q1 . (m + 1) ) or ( Q . k > Q . m & Q1 . k > Q1 . (m + 1) ) ) by A47, XREAL_1:9;
k < m + 1 by A45, NAT_1:13;
then ( ( (Part_sgn (Q1,K)) . {k,(m + 1)} = 1_ K & (Part_sgn (Q,K)) . x = 1_ K ) or ( (Part_sgn (Q1,K)) . {k,(m + 1)} = - (1_ K) & (Part_sgn (Q,K)) . x = - (1_ K) ) ) by A43, A44, A45, A46, A41, A50, A65, MATRIX11:def 1;
hence ((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q,K)) . x by A38, A42, A46, A64, FUNCT_1:12; :: thesis:

end;

suppose A66: ( Q1 . k < j & Q1 . (m + 1) >= j ) ; :: thesis:

m + 1 > i by A62, NAT_1:13;
then Q19 . (m + 1) <> j by A1, A2, A39, A50, FUNCT_1:def 4;
then A67: Q1 . (m + 1) > j by A66, XXREAL_0:1;
Q . m = (Q1 . (m + 1)) - 1 by A1, A2, A44, A62, A66, Def3;
then Q1 . (m + 1) = (Q . m) + 1 ;
then A68: Q . m >= j by A67, NAT_1:13;
Q1 . k = Q . k by A1, A2, A43, A62, A66, Def3;
then A69: Q . k < Q . m by A66, A68, XXREAL_0:2;
A70: k < m + 1 by A45, NAT_1:13;
Q1 . k < Q1 . (m + 1) by A66, XXREAL_0:2;
then (Part_sgn (Q1,K)) . {k,(m + 1)} = 1_ K by A43, A41, A50, A70, MATRIX11:def 1;
hence ((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q,K)) . x by A43, A44, A45, A46, A64, A63, A69, MATRIX11:def 1; :: thesis:

end;

suppose A71: ( Q1 . k >= j & Q1 . (m + 1) < j ) ; :: thesis:

then Q . k = (Q1 . k) - 1 by A1, A2, A43, A62, Def3;
then A72: Q1 . k = (Q . k) + 1 ;
Q19 . k <> j by A1, A2, A39, A43, A41, A62, FUNCT_1:def 4;
then Q1 . k > j by A71, XXREAL_0:1;
then A73: Q . k >= j by A72, NAT_1:13;
Q1 . (m + 1) = Q . m by A1, A2, A44, A62, A71, Def3;
then A74: Q . m < Q . k by A71, A73, XXREAL_0:2;
A75: k < m + 1 by A45, NAT_1:13;
Q1 . k > Q1 . (m + 1) by A71, XXREAL_0:2;
then (Part_sgn (Q1,K)) . {k,(m + 1)} = - (1_ K) by A43, A41, A50, A75, MATRIX11:def 1;
hence ((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q,K)) . x by A43, A44, A45, A46, A64, A63, A74, MATRIX11:def 1; :: thesis:

end;

suppose A76: ( k >= i & m >= i ) ; :: thesis:

A77: ((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q1,K)) . (f . {k,m}) by A38, A42, A46, FUNCT_1:12;
A78: k + 1 < m + 1 by A45, XREAL_1:6;
A79: f . {k,m} = {(k + 1),(m + 1)} by A37, A42, A45, A46, A76;

per cases ;

suppose ( ( Q1 . (k + 1) < j & Q1 . (m + 1) < j ) or ( Q1 . (k + 1) >= j & Q1 . (m + 1) >= j ) ) ; :: thesis:

then ( ( Q . k = Q1 . (k + 1) & Q . m = Q1 . (m + 1) ) or ( Q . k = (Q1 . (k + 1)) - 1 & Q . m = (Q1 . (m + 1)) - 1 ) ) by A1, A2, A43, A44, A76, Def3;
then ( ( Q . k < Q . m & Q1 . (k + 1) < Q1 . (m + 1) ) or ( Q . k > Q . m & Q1 . (k + 1) > Q1 . (m + 1) ) ) by A47, XREAL_1:9;
then ( ( (Part_sgn (Q1,K)) . {(k + 1),(m + 1)} = 1_ K & (Part_sgn (Q,K)) . x = 1_ K ) or ( (Part_sgn (Q1,K)) . {(m + 1),(k + 1)} = - (1_ K) & (Part_sgn (Q,K)) . x = - (1_ K) ) ) by A43, A44, A45, A46, A49, A50, A78, MATRIX11:def 1;
hence ((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q,K)) . x by A38, A42, A46, A79, FUNCT_1:12; :: thesis:

end;

suppose A80: ( Q1 . (k + 1) < j & Q1 . (m + 1) >= j ) ; :: thesis:

m + 1 > i by A76, NAT_1:13;
then Q19 . (m + 1) <> j by A1, A2, A39, A50, FUNCT_1:def 4;
then A81: Q1 . (m + 1) > j by A80, XXREAL_0:1;
Q . m = (Q1 . (m + 1)) - 1 by A1, A2, A44, A76, A80, Def3;
then Q1 . (m + 1) = (Q . m) + 1 ;
then A82: Q . m >= j by A81, NAT_1:13;
Q1 . (k + 1) < Q1 . (m + 1) by A80, XXREAL_0:2;
then A83: (Part_sgn (Q1,K)) . {(k + 1),(m + 1)} = 1_ K by A49, A50, A78, MATRIX11:def 1;
Q1 . (k + 1) = Q . k by A1, A2, A43, A76, A80, Def3;
then Q . k < Q . m by A80, A82, XXREAL_0:2;
hence ((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q,K)) . x by A43, A44, A45, A46, A79, A77, A83, MATRIX11:def 1; :: thesis:

end;

suppose A84: ( Q1 . (k + 1) >= j & Q1 . (m + 1) < j ) ; :: thesis:

k + 1 > i by A76, NAT_1:13;
then Q19 . (k + 1) <> j by A1, A2, A39, A49, FUNCT_1:def 4;
then A85: Q1 . (k + 1) > j by A84, XXREAL_0:1;
Q . k = (Q1 . (k + 1)) - 1 by A1, A2, A43, A76, A84, Def3;
then Q1 . (k + 1) = (Q . k) + 1 ;
then A86: Q . k >= j by A85, NAT_1:13;
Q1 . (k + 1) > Q1 . (m + 1) by A84, XXREAL_0:2;
then A87: (Part_sgn (Q1,K)) . {(k + 1),(m + 1)} = - (1_ K) by A49, A50, A78, MATRIX11:def 1;
Q1 . (m + 1) = Q . m by A1, A2, A44, A76, A84, Def3;
then Q . k > Q . m by A84, A86, XXREAL_0:2;
hence ((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q,K)) . x by A43, A44, A45, A46, A79, A77, A87, MATRIX11:def 1; :: thesis:

end;

reconsider domf = dom f as Element of Fin (2Set (Seg (n2 + 2))) by FINSUB_1:def 5;
A88: f .: domf = rng f by RELAT_1:113;
dom f = 2Set (Seg (n2 + 2)) by FUNCT_2:def 1;
then A89: domf = In ((2Set (Seg (n2 + 2))),(Fin (2Set (Seg (n2 + 2))))) by SUBSET_1:def 8;
dom (Part_sgn (Q,K)) = 2Set (Seg (n2 + 2)) by FUNCT_2:def 1;
then Part_sgn (Q,K) = (Part_sgn (Q1,K)) * f by A38, A40, FUNCT_1:2;
then A90: the multF of K $$ (SSX,(Part_sgn (Q1,K))) = sgn (Q,K) by A35, A36, A89, A88, SETWOP_2:6;
X misses SSX by XBOOLE_1:79;
then sgn (Q1,K) = ((power K) . ((- (1_ K)),(i + j))) * (sgn (Q,K)) by A31, A90, A34, A32, SETWOP_2:4;
hence - (a,p1) = (((power K) . ((- (1_ K)),(i + j))) * (sgn (Q,K))) * a by MATRIX11:26
.= ((power K) . ((- (1_ K)),(i + j))) * ((sgn (Q,K)) * a) by GROUP_1:def 3
.= ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i)))) by MATRIX11:26 ;
:: thesis:

end;