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)

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

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;

then A18: Sum q = q . ji by A12, MATRIX_3:12
.= 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

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;

then Sum (p | i) = (p | i) . i by A7, A11, MATRIX_3:12
.= 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;

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