let n be Nat; :: thesis: for K being Fanoian Field
for p2 being Element of Permutations (n + 2)
for i, j being Nat st i in Seg (n + 2) & p2 . i = j holds
ex X being Element of Fin (2Set (Seg (n + 2))) st
( X = { {N,i} where N is Element of NAT : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(i + j) )
let K be Fanoian Field; :: thesis: for p2 being Element of Permutations (n + 2)
for i, j being Nat st i in Seg (n + 2) & p2 . i = j holds
ex X being Element of Fin (2Set (Seg (n + 2))) st
( X = { {N,i} where N is Element of NAT : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(i + j) )
let p2 be Element of Permutations (n + 2); :: thesis: for i, j being Nat st i in Seg (n + 2) & p2 . i = j holds
ex X being Element of Fin (2Set (Seg (n + 2))) st
( X = { {N,i} where N is Element of NAT : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(i + j) )
let i, j be Nat; :: thesis: ( i in Seg (n + 2) & p2 . i = j implies ex X being Element of Fin (2Set (Seg (n + 2))) st
( X = { {N,i} where N is Element of NAT : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(i + j) ) )
assume A1: ( i in Seg (n + 2) & p2 . i = j ) ; :: thesis: ex X being Element of Fin (2Set (Seg (n + 2))) st
( X = { {N,i} where N is Element of NAT : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(i + j) )
reconsider N = n as Element of NAT by ORDINAL1:def 13;
set n2 = N + 2;
set X = { {k,i} where k is Element of NAT : {k,i} in 2Set (Seg (n + 2)) } ;
set SS = 2Set (Seg (n + 2));
set P = power K;
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 13;
reconsider p2' = p2 as Permutation of (finSeg (N + 2)) by MATRIX_2:def 11;
A2: { {k,i} where k is Element of NAT : {k,i} in 2Set (Seg (n + 2)) } c= 2Set (Seg (n + 2))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { {k,i} where k is Element of NAT : {k,i} in 2Set (Seg (n + 2)) } or x in 2Set (Seg (n + 2)) )
assume x in { {k,i} where k is Element of NAT : {k,i} in 2Set (Seg (n + 2)) } ; :: thesis: x in 2Set (Seg (n + 2))
then ex k being Element of NAT st
( x = {k,i} & {k,i} in 2Set (Seg (N + 2)) ) ;
hence x in 2Set (Seg (n + 2)) ; :: thesis: verum

end;

reconsider X = { {k,i} where k is Element of NAT : {k,i} in 2Set (Seg (n + 2)) } as Element of Fin (2Set (Seg (n + 2))) by A2, FINSUB_1:def 5;
take X ; :: thesis: ( X = { {N,i} where N is Element of NAT : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(i + j) )
thus X = { {e,i} where e is Element of NAT : {e,i} in 2Set (Seg (n + 2)) } ; :: thesis: the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(i + j)
set Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s = - (1_ K) ) } ;
A3: { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s = - (1_ K) ) } c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s = - (1_ K) ) } or x in X )
assume x in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s = - (1_ K) ) } ; :: thesis: x in X
then ex s being Element of 2Set (Seg (n + 2)) st
( s = x & s in X & (Part_sgn p2,K) . s = - (1_ K) ) ;
hence x in X ; :: thesis: verum

end;

then ( { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s = - (1_ K) ) } c= 2Set (Seg (n + 2)) & { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s = - (1_ K) ) } is finite ) by A2, XBOOLE_1:1;
then reconsider Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s = - (1_ K) ) } as Element of Fin (2Set (Seg (n + 2))) by FINSUB_1:def 5;
1 <= i by A1, FINSEQ_1:3;
then reconsider i1 = i - 1 as Element of NAT by NAT_1:21;
set Li = finSeg i1;
set Ui = (finSeg (N + 2)) \ (Seg i);
i1 < i1 + 1 by NAT_1:13;
then ( finSeg i1 c= Seg i & Seg i misses (finSeg (N + 2)) \ (Seg i) ) by FINSEQ_1:7, XBOOLE_1:79;
then A4: finSeg i1 misses (finSeg (N + 2)) \ (Seg i) by XBOOLE_1:64;
A5: (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) c= (Seg (N + 2)) \ {i}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) or x in (Seg (N + 2)) \ {i} )
assume A6: x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) ; :: thesis: x in (Seg (N + 2)) \ {i}

per cases ( x in finSeg i1 or x in (finSeg (N + 2)) \ (Seg i) ) by A6, XBOOLE_0:def 3;

suppose x in finSeg i1 ; :: thesis: x in (Seg (N + 2)) \ {i}

then consider k being Element of NAT such that
A7: ( x = k & 1 <= k & k <= i1 ) ;
( k <= i1 & i1 < i1 + 1 ) by A7, NAT_1:13;
then ( k < i & i <= N + 2 ) by A1, FINSEQ_1:3, XXREAL_0:2;
then ( not k in {i} & k <= N + 2 ) by TARSKI:def 1, XXREAL_0:2;
then ( not k in {i} & k in Seg (N + 2) ) by A7;
hence x in (Seg (N + 2)) \ {i} by A7, XBOOLE_0:def 5; :: thesis: verum

end;

suppose x in (finSeg (N + 2)) \ (Seg i) ; :: thesis: x in (Seg (N + 2)) \ {i}

then ( x in Seg (N + 2) & not x in Seg i & i1 + 1 in Seg i ) by FINSEQ_1:6, XBOOLE_0:def 5;
then ( x in Seg (N + 2) & not x in {i} ) by TARSKI:def 1;
hence x in (Seg (N + 2)) \ {i} by XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

(finSeg (N + 2)) \ {i} c= (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (finSeg (N + 2)) \ {i} or x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) )
assume A8: x in (finSeg (N + 2)) \ {i} ; :: thesis: x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i))
x in finSeg (N + 2) by A8;
then consider k being Element of NAT such that
A9: ( x = k & 1 <= k & k <= N + 2 ) ;
not k in {i} by A8, A9, XBOOLE_0:def 5;
then A10: k <> i by TARSKI:def 1;

per cases ( k < i1 + 1 or k > i1 + 1 ) by A10, XXREAL_0:1;

suppose k < i1 + 1 ; :: thesis: x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i))

then k <= i1 by NAT_1:13;
then x in finSeg i1 by A9;
hence x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose k > i1 + 1 ; :: thesis: x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i))

then ( not x in Seg i & x in Seg (N + 2) ) by A9, FINSEQ_1:3;
then x in (finSeg (N + 2)) \ (Seg i) by XBOOLE_0:def 5;
hence x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then A11: (finSeg (N + 2)) \ {i} = (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) by A5, XBOOLE_0:def 10;
deffunc H₁( set ) -> set = {$1,i};
consider f being Function such that
A12: ( dom f = (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) & ( for x being set st x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
A13: rng f c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in X )
assume x in rng f ; :: thesis: x in X
then consider y being set such that
A14: ( y in dom f & f . y = x ) by FUNCT_1:def 5;
y in finSeg (N + 2) by A11, A12, A14;
then consider k being Element of NAT such that
A15: ( k = y & 1 <= k & k <= N + 2 ) ;
not y in {i} by A5, A12, A14, XBOOLE_0:def 5;
then i <> k by A15, TARSKI:def 1;
then ( k in Seg (N + 2) & ( k < i or i < k ) ) by A15, XXREAL_0:1;
then ( {i,k} in 2Set (Seg (n + 2)) & f . k = {i,k} ) by A1, A12, A14, A15, MATRIX11:1;
hence x in X by A14, A15; :: thesis: verum

end;

A16: X c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in rng f )
assume x in X ; :: thesis: x in rng f
then consider k being Element of NAT such that
A17: ( x = {k,i} & {k,i} in 2Set (Seg (n + 2)) ) ;
k <> i by A17, SGRAPH1:12;
then ( k in Seg (N + 2) & not k in {i} ) by A17, SGRAPH1:12, TARSKI:def 1;
then k in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) by A11, XBOOLE_0:def 5;
then ( k in dom f & f . k = H₁(k) ) by A12;
hence x in rng f by A17, FUNCT_1:def 5; :: thesis: verum

end;

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 A18: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
( not x1 in {i} & f . x1 = H₁(x1) & f . x2 = H₁(x2) ) by A5, A12, A18, XBOOLE_0:def 5;
then ( x1 <> i & x1 in {i,x2} ) by A18, TARSKI:def 1, TARSKI:def 2;
hence x1 = x2 by TARSKI:def 2; :: thesis: verum

end;

then A19: f is one-to-one by FUNCT_1:def 8;
dom p2' = Seg (N + 2) by FUNCT_2:67;
then A20: ( p2 . i in rng p2 & rng p2' = Seg (N + 2) ) by A1, FUNCT_1:def 5, FUNCT_2:def 3;
then 1 <= j by A1, FINSEQ_1:3;
then reconsider j1 = j - 1 as Element of NAT by NAT_1:21;
A21: p2' .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) c= Seg j1

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in p2' .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) or y in Seg j1 )
assume y in p2' .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) ; :: thesis: y in Seg j1
then consider x being set such that
A22: ( x in dom p2' & x in ((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) & p2' . x = y ) by FUNCT_1:def 12;
dom p2' = Seg (N + 2) by FUNCT_2:67;
then consider k being Element of NAT such that
A23: ( x = k & 1 <= k & k <= N + 2 ) by A22;

per cases ( k in (finSeg i1) \ (f " Y) or k in ((finSeg (N + 2)) \ (Seg i)) /\ (f " Y) ) by A22, A23, XBOOLE_0:def 3;

suppose A24: k in (finSeg i1) \ (f " Y) ; :: thesis: y in Seg j1

then ( k in finSeg i1 & finSeg i1 c= dom f ) by A12, XBOOLE_1:7;
then ( k in dom f & not k in f " Y & k <= i1 ) by A24, FINSEQ_1:3, XBOOLE_0:def 5;
then A25: ( not f . k in Y & f . k in rng f & f . k = H₁(k) & k < i1 + 1 ) by A12, FUNCT_1:def 5, FUNCT_1:def 13, NAT_1:13;
then H₁(k) in X by A13;
then consider m being Element of NAT such that
A26: ( H₁(k) = {m,i} & {m,i} in 2Set (Seg (n + 2)) ) ;
( (Part_sgn p2,K) . {k,i} <> - (1_ K) & k in Seg (N + 2) & dom p2' = Seg (N + 2) ) by A13, A23, A25, A26, FUNCT_2:67;
then ( p2 . k <= p2 . i & p2 . i <> p2 . k ) by A1, A25, FUNCT_1:def 8, MATRIX11:def 1;
then ( p2 . k < j1 + 1 & p2 . k in rng p2' & rng p2' = Seg (N + 2) ) by A1, A22, A23, FUNCT_1:def 5, FUNCT_2:def 3, XXREAL_0:1;
then ( p2 . k <= j1 & 1 <= p2 . k ) by FINSEQ_1:3, NAT_1:13;
hence y in Seg j1 by A22, A23, FINSEQ_1:3; :: thesis: verum

end;

suppose A27: k in ((finSeg (N + 2)) \ (Seg i)) /\ (f " Y) ; :: thesis: y in Seg j1

then k in f " Y by XBOOLE_0:def 4;
then A28: ( k in dom f & f . k in Y ) by FUNCT_1:def 13;
then consider s being Element of 2Set (Seg (n + 2)) such that
A29: ( s = f . k & s in X & (Part_sgn p2,K) . s = - (1_ K) ) ;
k in (finSeg (N + 2)) \ (Seg i) by A27, XBOOLE_0:def 4;
then ( k in Seg (N + 2) & not k in Seg i ) by XBOOLE_0:def 5;
then ( 1 <= k & ( 1 > k or k > i ) ) by FINSEQ_1:3;
then ( s = {i,k} & i < k & 1_ K <> - (1_ K) & dom p2' = finSeg (N + 2) ) by A12, A28, A29, FUNCT_2:67, MATRIX11:22;
then ( p2 . i >= p2 . k & p2' . i <> p2 . k ) by A1, A27, A29, FUNCT_1:def 8, MATRIX11:def 1;
then ( p2 . k < j1 + 1 & p2 . k in rng p2' & rng p2' = Seg (N + 2) ) by A1, A22, A23, FUNCT_1:def 5, FUNCT_2:def 3, XXREAL_0:1;
then ( p2 . k <= j1 & 1 <= p2 . k ) by FINSEQ_1:3, NAT_1:13;
hence y in Seg j1 by A22, A23, FINSEQ_1:3; :: thesis: verum

end;

end;

end;

A30: Seg j1 c= p2' .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)))

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Seg j1 or y in p2' .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) )
assume A31: y in Seg j1 ; :: thesis: y in p2' .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)))
consider k being Element of NAT such that
A32: ( y = k & 1 <= k & k <= j1 ) by A31;
A33: ( j <= N + 2 & j1 < j1 + 1 ) by A1, A20, FINSEQ_1:3, NAT_1:13;
then A34: ( j1 <= N + 2 & k < j ) by A32, XXREAL_0:2;
then Seg j1 c= Seg (N + 2) by FINSEQ_1:7;
then consider x being set such that
A35: ( x in dom p2' & y = p2' . x ) by A20, A31, FUNCT_1:def 5;
A36: not x in {i} by A1, A32, A33, A35, TARSKI:def 1;
then x in dom f by A11, A12, A35, XBOOLE_0:def 5;
then A37: ( f . x = H₁(x) & f . x in rng f ) by A12, FUNCT_1:def 5;
then H₁(x) in X by A13;
then consider m being Element of NAT such that
A38: ( H₁(x) = {m,i} & {m,i} in 2Set (Seg (N + 2)) ) ;
A39: ( m in {x,i} & m <> i ) by A38, SGRAPH1:12, TARSKI:def 2;
then A40: ( m = x & m <> i & m in Seg (N + 2) ) by A38, SGRAPH1:12, TARSKI:def 2;

per cases ( m < i or m > i ) by A39, XXREAL_0:1;

suppose A41: m < i ; :: thesis: y in p2' .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)))

A42: not m in f " Y

proof

assume m in f " Y ; :: thesis: contradiction
then {m,i} in Y by A37, A40, FUNCT_1:def 13;
then ( ex s being Element of 2Set (Seg (n + 2)) st
( s = {m,i} & s in X & (Part_sgn p2,K) . s = - (1_ K) ) & (Part_sgn p2,K) . {m,i} = 1_ K ) by A1, A32, A34, A35, A40, A41, MATRIX11:def 1;
hence contradiction by MATRIX11:22; :: thesis: verum

end;

m < i1 + 1 by A41;
then ( m <= i1 & 1 <= m ) by A40, FINSEQ_1:3, NAT_1:13;
then m in finSeg i1 ;
then x in (finSeg i1) \ (f " Y) by A40, A42, XBOOLE_0:def 5;
then x in ((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) by XBOOLE_0:def 3;
hence y in p2' .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) by A35, FUNCT_1:def 12; :: thesis: verum

end;

suppose A43: m > i ; :: thesis: y in p2' .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)))

then (Part_sgn p2,K) . {m,i} = - (1_ K) by A1, A32, A34, A35, A40, MATRIX11:def 1;
then ( f . x in Y & x in dom f & not m in Seg i ) by A11, A12, A13, A35, A36, A37, A38, A43, FINSEQ_1:3, XBOOLE_0:def 5;
then ( x in f " Y & x in (finSeg (N + 2)) \ (Seg i) ) by A40, FUNCT_1:def 13, XBOOLE_0:def 5;
then x in ((finSeg (N + 2)) \ (Seg i)) /\ (f " Y) by XBOOLE_0:def 4;
then x in ((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) by XBOOLE_0:def 3;
hence y in p2' .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) by A35, FUNCT_1:def 12; :: thesis: verum

end;

end;

end;

( (finSeg i1) \ (f " Y) c= finSeg i1 & (finSeg i1) /\ (f " Y) c= finSeg i1 & ((finSeg (N + 2)) \ (Seg i)) /\ (f " Y) c= (finSeg (N + 2)) \ (Seg i) ) by XBOOLE_1:17;
then A44: ( (finSeg i1) \ (f " Y) misses ((finSeg (N + 2)) \ (Seg i)) /\ (f " Y) & (finSeg i1) /\ (f " Y) misses ((finSeg (N + 2)) \ (Seg i)) /\ (f " Y) & ((finSeg i1) /\ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) = (dom f) /\ (f " Y) & f " Y c= dom f & (f " Y) /\ (finSeg i1) c= finSeg i1 & ((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) c= (finSeg (N + 2)) \ {i} & (finSeg i1) \ (f " Y) = (finSeg i1) \ ((f " Y) /\ (finSeg i1)) ) by A4, A11, A12, RELAT_1:167, XBOOLE_1:13, XBOOLE_1:23, XBOOLE_1:47, XBOOLE_1:64;
then A45: ( ((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) c= Seg (N + 2) & Seg (N + 2) = dom p2' & ((finSeg i1) /\ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) = f " Y ) by FUNCT_2:67, XBOOLE_1:1, XBOOLE_1:28;
reconsider fY = f " Y as finite set by A44, XBOOLE_1:28;
( f .: fY,fY are_equipotent & X = rng f ) by A13, A16, A19, A44, CARD_1:60, XBOOLE_0:def 10;
then A46: ( card (f .: fY) = card fY & f .: fY = Y ) by A3, CARD_1:21, FUNCT_1:147;
Seg j1 = p2' .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) by A21, A30, XBOOLE_0:def 10;
then finSeg j1,((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) are_equipotent by A45, CARD_1:60;
then A47: card (finSeg j1) = card (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) by CARD_1:21
.= (card ((finSeg i1) \ ((f " Y) /\ (finSeg i1)))) + (card (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) by A44, CARD_2:53
.= ((card (finSeg i1)) - (card ((f " Y) /\ (finSeg i1)))) + (card (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) by CARD_2:63, XBOOLE_1:17 ;

per cases ( j > i or j <= i ) ;

suppose j > i ; :: thesis: the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(i + j)

then reconsider ji = j - i as Element of NAT by NAT_1:21;
card Y = (((card ((finSeg i1) /\ fY)) + (card (finSeg j1))) - (card (finSeg i1))) + (card (fY /\ (finSeg i1))) by A44, A45, A46, A47, CARD_2:53
.= ((2 * (card ((finSeg i1) /\ fY))) + (card (finSeg j1))) - (card (finSeg i1))
.= ((2 * (card ((finSeg i1) /\ fY))) + j1) - (card (finSeg i1)) by FINSEQ_1:78
.= ((2 * (card ((finSeg i1) /\ fY))) + j1) - i1 by FINSEQ_1:78
.= (2 * (card ((finSeg i1) /\ fY))) + ji ;
hence the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),((2 * (card ((finSeg i1) /\ fY))) + ji) by Th8
.= ((power K) . (- (1_ K)),(2 * (card ((finSeg i1) /\ fY)))) * ((power K) . (- (1_ K)),ji) by HURWITZ:3
.= (1_ K) * ((power K) . (- (1_ K)),ji) by HURWITZ:4
.= ((power K) . (- (1_ K)),(2 * I)) * ((power K) . (- (1_ K)),ji) by HURWITZ:4
.= (power K) . (- (1_ K)),((2 * i) + ji) by HURWITZ:3
.= (power K) . (- (1_ K)),(i + j) ;
:: thesis: verum

end;

suppose j <= i ; :: thesis: the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(i + j)

then reconsider ij = i - j as Element of NAT by NAT_1:21;
card Y = (((card (finSeg i1)) + (card (((finSeg (N + 2)) \ (Seg i)) /\ fY))) - (card (finSeg j1))) + (card (((finSeg (N + 2)) \ (Seg i)) /\ fY)) by A44, A45, A46, A47, CARD_2:53
.= ((2 * (card (((finSeg (N + 2)) \ (Seg i)) /\ fY))) - (card (finSeg j1))) + (card (finSeg i1))
.= ((2 * (card (((finSeg (N + 2)) \ (Seg i)) /\ fY))) - j1) + (card (finSeg i1)) by FINSEQ_1:78
.= ((2 * (card (((finSeg (N + 2)) \ (Seg i)) /\ fY))) - j1) + i1 by FINSEQ_1:78
.= (2 * (card (((finSeg (N + 2)) \ (Seg i)) /\ fY))) + ij ;
hence the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),((2 * (card (((finSeg (N + 2)) \ (Seg i)) /\ fY))) + ij) by Th8
.= ((power K) . (- (1_ K)),(2 * (card (((finSeg (N + 2)) \ (Seg i)) /\ fY)))) * ((power K) . (- (1_ K)),ij) by HURWITZ:3
.= (1_ K) * ((power K) . (- (1_ K)),ij) by HURWITZ:4
.= ((power K) . (- (1_ K)),(2 * J)) * ((power K) . (- (1_ K)),ij) by HURWITZ:4
.= (power K) . (- (1_ K)),((2 * j) + ij) by HURWITZ:3
.= (power K) . (- (1_ K)),(i + j) ;
:: thesis: verum

end;

end;