let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for p being FinSequence of K

for i, j being Nat st i in dom p & j in dom p & i <> j & ( for k being Nat st k in dom p & k <> i & k <> j holds

p . k = 0. K ) holds

Sum p = (p /. i) + (p /. j)

let p be FinSequence of K; :: thesis: for i, j being Nat st i in dom p & j in dom p & i <> j & ( for k being Nat st k in dom p & k <> i & k <> j holds

p . k = 0. K ) holds

Sum p = (p /. i) + (p /. j)

p . k = 0. K ) implies Sum p = (p /. i) + (p /. j) )

assume that

A23: ( i in dom p & j in dom p ) and

A24: i <> j and

A25: for k being Nat st k in dom p & k <> i & k <> j holds

p . k = 0. K ; :: thesis: Sum p = (p /. i) + (p /. j)

A26: ( i < j or j < i ) by A24, XXREAL_0:1;

for k being Nat st k in dom p & k <> j & k <> i holds

p . k = 0. K by A25;

hence Sum p = (p /. i) + (p /. j) by A1, A23, A25, A26; :: thesis: verum

for i, j being Nat st i in dom p & j in dom p & i <> j & ( for k being Nat st k in dom p & k <> i & k <> j holds

p . k = 0. K ) holds

Sum p = (p /. i) + (p /. j)

let p be FinSequence of K; :: thesis: for i, j being Nat st i in dom p & j in dom p & i <> j & ( for k being Nat st k in dom p & k <> i & k <> j holds

p . k = 0. K ) holds

Sum p = (p /. i) + (p /. j)

A1: now :: thesis: for i, j being Nat st i in dom p & j in dom p & i < j & ( for k being Nat st k in dom p & k <> i & k <> j holds

p . k = 0. K ) holds

Sum p = (p /. i) + (p /. j)

let i, j be Nat; :: thesis: ( i in dom p & j in dom p & i <> j & ( for k being Nat st k in dom p & k <> i & k <> j holds p . k = 0. K ) holds

Sum p = (p /. i) + (p /. j)

let i, j be Nat; :: thesis: ( i in dom p & j in dom p & i < j & ( for k being Nat st k in dom p & k <> i & k <> j holds

p . k = 0. K ) implies Sum p = (p /. i) + (p /. j) )

assume that

A2: i in dom p and

A3: j in dom p and

A4: i < j and

A5: for k being Nat st k in dom p & k <> i & k <> j holds

p . k = 0. K ; :: thesis: Sum p = (p /. i) + (p /. j)

A6: dom p = Seg (len p) by FINSEQ_1:def 3;

then ( i in NAT & 1 <= i ) by A2, FINSEQ_1:1;

then A7: i in Seg i ;

set pI = p | i;

consider q being FinSequence such that

A8: p = (p | i) ^ q by FINSEQ_1:80;

reconsider q = q as FinSequence of K by A8, FINSEQ_1:36;

A9: i <= len p by A2, A6, FINSEQ_1:1;

then A10: len (p | i) = i by FINSEQ_1:17;

A11: dom (p | i) = Seg i by A9, FINSEQ_1:17;

then not j in dom (p | i) by A4, FINSEQ_1:1;

then consider ji being Nat such that

A12: ji in dom q and

A13: j = i + ji by A3, A8, A10, FINSEQ_1:25;

.= p . j by A8, A10, A12, A13, FINSEQ_1:def 7

.= p /. j by A3, PARTFUN1:def 6 ;

A19: Seg i c= Seg (len p) by A9, FINSEQ_1:5;

.= p . i by A8, A7, A11, FINSEQ_1:def 7

.= p /. i by A6, A7, A19, PARTFUN1:def 6 ;

hence Sum p = (p /. i) + (p /. j) by A8, A18, RLVECT_1:41; :: thesis: verum

end;p . k = 0. K ) implies Sum p = (p /. i) + (p /. j) )

assume that

A2: i in dom p and

A3: j in dom p and

A4: i < j and

A5: for k being Nat st k in dom p & k <> i & k <> j holds

p . k = 0. K ; :: thesis: Sum p = (p /. i) + (p /. j)

A6: dom p = Seg (len p) by FINSEQ_1:def 3;

then ( i in NAT & 1 <= i ) by A2, FINSEQ_1:1;

then A7: i in Seg i ;

set pI = p | i;

consider q being FinSequence such that

A8: p = (p | i) ^ q by FINSEQ_1:80;

reconsider q = q as FinSequence of K by A8, FINSEQ_1:36;

A9: i <= len p by A2, A6, FINSEQ_1:1;

then A10: len (p | i) = i by FINSEQ_1:17;

A11: dom (p | i) = Seg i by A9, FINSEQ_1:17;

then not j in dom (p | i) by A4, FINSEQ_1:1;

then consider ji being Nat such that

A12: ji in dom q and

A13: j = i + ji by A3, A8, A10, FINSEQ_1:25;

now :: thesis: for k being Nat st k in dom q & k <> ji holds

q . k = 0. K

then A18: Sum q =
q . ji
by A12, MATRIX_3:12
q . k = 0. K

let k be Nat; :: thesis: ( k in dom q & k <> ji implies q . k = 0. K )

assume that

A14: k in dom q and

A15: k <> ji ; :: thesis: q . k = 0. K

reconsider kk = k as Element of NAT by ORDINAL1:def 12;

A16: i + kk <> i + ji by A15;

dom q = Seg (len q) by FINSEQ_1:def 3;

then k >= 1 by A14, FINSEQ_1:1;

then k + i >= i + 1 by XREAL_1:7;

then A17: i + kk <> i by NAT_1:13;

thus q . k = p . (i + kk) by A8, A10, A14, FINSEQ_1:def 7

.= 0. K by A5, A8, A10, A13, A14, A17, A16, FINSEQ_1:28 ; :: thesis: verum

end;assume that

A14: k in dom q and

A15: k <> ji ; :: thesis: q . k = 0. K

reconsider kk = k as Element of NAT by ORDINAL1:def 12;

A16: i + kk <> i + ji by A15;

dom q = Seg (len q) by FINSEQ_1:def 3;

then k >= 1 by A14, FINSEQ_1:1;

then k + i >= i + 1 by XREAL_1:7;

then A17: i + kk <> i by NAT_1:13;

thus q . k = p . (i + kk) by A8, A10, A14, FINSEQ_1:def 7

.= 0. K by A5, A8, A10, A13, A14, A17, A16, FINSEQ_1:28 ; :: thesis: verum

.= p . j by A8, A10, A12, A13, FINSEQ_1:def 7

.= p /. j by A3, PARTFUN1:def 6 ;

A19: Seg i c= Seg (len p) by A9, FINSEQ_1:5;

now :: thesis: for k being Nat st k in dom (p | i) & k <> i holds

(p | i) . k = 0. K

then Sum (p | i) =
(p | i) . i
by A7, A11, MATRIX_3:12
(p | i) . k = 0. K

let k be Nat; :: thesis: ( k in dom (p | i) & k <> i implies (p | i) . k = 0. K )

assume that

A20: k in dom (p | i) and

A21: k <> i ; :: thesis: (p | i) . k = 0. K

reconsider kk = k as Element of NAT by ORDINAL1:def 12;

A22: k <> j by A4, A11, A20, FINSEQ_1:1;

thus (p | i) . k = p . kk by A8, A20, FINSEQ_1:def 7

.= 0. K by A5, A6, A11, A19, A20, A21, A22 ; :: thesis: verum

end;assume that

A20: k in dom (p | i) and

A21: k <> i ; :: thesis: (p | i) . k = 0. K

reconsider kk = k as Element of NAT by ORDINAL1:def 12;

A22: k <> j by A4, A11, A20, FINSEQ_1:1;

thus (p | i) . k = p . kk by A8, A20, FINSEQ_1:def 7

.= 0. K by A5, A6, A11, A19, A20, A21, A22 ; :: thesis: verum

.= p . i by A8, A7, A11, FINSEQ_1:def 7

.= p /. i by A6, A7, A19, PARTFUN1:def 6 ;

hence Sum p = (p /. i) + (p /. j) by A8, A18, RLVECT_1:41; :: thesis: verum

p . k = 0. K ) implies Sum p = (p /. i) + (p /. j) )

assume that

A23: ( i in dom p & j in dom p ) and

A24: i <> j and

A25: for k being Nat st k in dom p & k <> i & k <> j holds

p . k = 0. K ; :: thesis: Sum p = (p /. i) + (p /. j)

A26: ( i < j or j < i ) by A24, XXREAL_0:1;

for k being Nat st k in dom p & k <> j & k <> i holds

p . k = 0. K by A25;

hence Sum p = (p /. i) + (p /. j) by A1, A23, A25, A26; :: thesis: verum