let n be Nat; :: thesis: for p1 being Element of Permutations (n + 1)

for K being Field

for a being Element of K

for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds

- (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

let p1 be Element of Permutations (n + 1); :: thesis: for K being Field

for a being Element of K

for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds

- (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

let K be Field; :: thesis: for a being Element of K

for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds

- (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

let a be Element of K; :: thesis: for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds

- (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

set n1 = n + 1;

let i, j be Nat; :: thesis: ( i in Seg (n + 1) & p1 . i = j implies - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i)))) )

assume that

A1: i in Seg (n + 1) and

A2: p1 . i = j ; :: thesis: - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

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);

for K being Field

for a being Element of K

for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds

- (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

let p1 be Element of Permutations (n + 1); :: thesis: for K being Field

for a being Element of K

for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds

- (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

let K be Field; :: thesis: for a being Element of K

for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds

- (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

let a be Element of K; :: thesis: for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds

- (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

set n1 = n + 1;

let i, j be Nat; :: thesis: ( i in Seg (n + 1) & p1 . i = j implies - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i)))) )

assume that

A1: i in Seg (n + 1) and

A2: p1 . i = j ; :: thesis: - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

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
( n = 0 or n = 1 or n >= 2 )
by NAT_1:23;

end;

suppose A6:
n = 0
; :: thesis: - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

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: verum

end;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: verum

suppose A11:
n = 1
; :: thesis: - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

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

end;per cases
( p1 = <*1,2*> or p1 = <*2,1*> )
by A12, MATRIX_7:1;

end;

suppose A13:
p1 = <*1,2*>
; :: thesis: - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

( 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, FINSEQ_1:44;

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: verum

end;then ( ( i = 1 & p1 . i = 1 ) or ( i = 2 & p1 . i = 2 ) ) by A13, FINSEQ_1:44;

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: verum

suppose A17:
p1 = <*2,1*>
; :: thesis: - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

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, FINSEQ_1:44;

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: verum

end;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, FINSEQ_1:44;

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: verum

suppose A20:
n >= 2
; :: thesis: - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

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

end;per cases
( not K is Fanoian or K is Fanoian )
;

end;

suppose A21:
not K is Fanoian
; :: thesis: - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

- (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: verum

end;

A22: now :: thesis: (power K) . ((- (1_ K)),(i + j)) = 1_ Kend;

A26:
( - (a,p1) = a or - (a,p1) = - a )
by MATRIX_1:def 16;per cases
( (i + j) mod 2 = 0 or (i + j) mod 2 = 1 )
by NAT_D:12;

end;

suppose
(i + j) mod 2 = 0
; :: thesis: (power K) . ((- (1_ K)),(i + j)) = 1_ K

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: verum

end;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: verum

suppose
(i + j) mod 2 = 1
; :: thesis: (power K) . ((- (1_ K)),(i + j)) = 1_ K

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: verum

end;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: verum

- (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: verum

suppose A29:
K is Fanoian
; :: thesis: - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))

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;

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: verum

end;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: for x being object st x in 2Set (Seg (n2 + 2)) holds

((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q,K)) . x

reconsider domf = dom f as Element of Fin (2Set (Seg (n2 + 2))) by FINSUB_1:def 5;((Part_sgn (Q1,K)) * f) . x = (Part_sgn (Q,K)) . x

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: ( x in 2Set (Seg (n2 + 2)) implies ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1} )

assume A42: x in 2Set (Seg (n2 + 2)) ; :: thesis: ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1}

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;

end;then A41: Seg (n2 + 2) c= Seg (n1 + 2) by FINSEQ_1:5;

let x be object ; :: thesis: ( x in 2Set (Seg (n2 + 2)) implies ((Part_sgn (Q1,K)) * f) . b

assume A42: x in 2Set (Seg (n2 + 2)) ; :: thesis: ((Part_sgn (Q1,K)) * f) . b

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
( ( k < i & m < i ) or ( k >= i & m < i ) or ( k < i & m >= i ) or ( k >= i & m >= i ) )
;

end;

suppose A51:
( k < i & m < i )
; :: thesis: ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1}

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;

end;A53: f . x = x by A37, A42, A45, A46, A51;

per cases
( ( Q1 . k < j & Q1 . m < j ) or ( Q1 . k >= j & Q1 . m >= j ) or ( Q1 . k < j & Q1 . m >= j ) or ( Q1 . k >= j & Q1 . m < j ) )
;

end;

suppose
( ( Q1 . k < j & Q1 . m < j ) or ( Q1 . k >= j & Q1 . m >= j ) )
; :: thesis: ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1}

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: verum

end;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: verum

suppose A54:
( Q1 . k < j & Q1 . m >= j )
; :: thesis: ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1}

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: verum

end;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: verum

suppose A58:
( Q1 . k >= j & Q1 . m < j )
; :: thesis: ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1}

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: verum

end;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: verum

suppose
( k >= i & m < i )
; :: thesis: ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1}

end;

end;

suppose A62:
( k < i & m >= i )
; :: thesis: ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1}

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;

end;A64: f . {k,m} = {k,(m + 1)} by A37, A42, A45, A46, A62;

per cases
( ( Q1 . k < j & Q1 . (m + 1) < j ) or ( Q1 . k >= j & Q1 . (m + 1) >= j ) or ( Q1 . k < j & Q1 . (m + 1) >= j ) or ( Q1 . k >= j & Q1 . (m + 1) < j ) )
;

end;

suppose
( ( Q1 . k < j & Q1 . (m + 1) < j ) or ( Q1 . k >= j & Q1 . (m + 1) >= j ) )
; :: thesis: ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1}

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: verum

end;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: verum

suppose A66:
( Q1 . k < j & Q1 . (m + 1) >= j )
; :: thesis: ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1}

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: verum

end;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: verum

suppose A71:
( Q1 . k >= j & Q1 . (m + 1) < j )
; :: thesis: ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1}

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: verum

end;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: verum

suppose A76:
( k >= i & m >= i )
; :: thesis: ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1}

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;

end;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
( ( Q1 . (k + 1) < j & Q1 . (m + 1) < j ) or ( Q1 . (k + 1) >= j & Q1 . (m + 1) >= j ) or ( Q1 . (k + 1) < j & Q1 . (m + 1) >= j ) or ( Q1 . (k + 1) >= j & Q1 . (m + 1) < j ) )
;

end;

suppose
( ( Q1 . (k + 1) < j & Q1 . (m + 1) < j ) or ( Q1 . (k + 1) >= j & Q1 . (m + 1) >= j ) )
; :: thesis: ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1}

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: verum

end;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: verum

suppose A80:
( Q1 . (k + 1) < j & Q1 . (m + 1) >= j )
; :: thesis: ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1}

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: verum

end;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: verum

suppose A84:
( Q1 . (k + 1) >= j & Q1 . (m + 1) < j )
; :: thesis: ((Part_sgn (Q1,K)) * f) . b_{1} = (Part_sgn (Q,K)) . b_{1}

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: verum

end;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: verum

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: verum