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

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 & j in dom p & i < j ) and
A3: 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)
set pI = p | i;
consider q being FinSequence such that
A4: p = (p | i) ^ q by FINSEQ_1:101;
reconsider q = q as FinSequence of K by A4, FINSEQ_1:50;
A5: dom p = Seg (len p) by FINSEQ_1:def 3;
A6: i in NAT by ORDINAL1:def 13;
( 1 <= i & i <= len p ) by A5, A2, FINSEQ_1:3;
then A7: ( i in Seg i & len (p | i) = i & dom (p | i) = Seg i & Seg i c= Seg (len p) ) by A6, FINSEQ_1:7, FINSEQ_1:21;

now

let k be Nat; :: thesis: ( k in dom (p | i) & k <> i implies (p | i) . k = 0. K )
assume A8: ( k in dom (p | i) & k <> i ) ; :: thesis: (p | i) . k = 0. K
reconsider kk = k as Element of NAT by ORDINAL1:def 13;
A9: k <> j by A2, A7, A8, FINSEQ_1:3;
thus (p | i) . k = p . kk by A4, A8, FINSEQ_1:def 7
.= 0. K by A5, A7, A3, A8, A9 ; :: thesis: verum

end;

then A10: Sum (p | i) = (p | i) . i by A7, MATRIX_3:14
.= p . i by A4, A7, FINSEQ_1:def 7
.= p /. i by A5, A7, PARTFUN1:def 8 ;
not j in dom (p | i) by A2, A7, FINSEQ_1:3;
then consider ji being Nat such that
A11: ( ji in dom q & j = i + ji ) by A7, A2, A4, FINSEQ_1:38;

now

let k be Nat; :: thesis: ( k in dom q & k <> ji implies q . k = 0. K )
assume A12: ( k in dom q & k <> ji ) ; :: thesis: q . k = 0. K
reconsider kk = k as Element of NAT by ORDINAL1:def 13;
dom q = Seg (len q) by FINSEQ_1:def 3;
then k >= 1 by A12, FINSEQ_1:3;
then k + i >= i + 1 by XREAL_1:9;
then A13: ( i + kk <> i & i + kk <> i + ji ) by A12, NAT_1:13;
thus q . k = p . (i + kk) by A4, A7, A12, FINSEQ_1:def 7
.= 0. K by A3, A11, A13, A4, A7, A12, FINSEQ_1:41 ; :: thesis: verum

end;

then Sum q = q . ji by A11, MATRIX_3:14
.= p . j by A11, A7, A4, FINSEQ_1:def 7
.= p /. j by A2, PARTFUN1:def 8 ;
hence Sum p = (p /. i) + (p /. j) by A10, A4, RLVECT_1:58; :: 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
A14: ( i in dom p & j in dom p & i <> j ) and
A15: 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)
A16: for k being Nat st k in dom p & k <> j & k <> i holds
p . k = 0. K by A15;
( i < j or j < i ) by A14, XXREAL_0:1;
hence Sum p = (p /. i) + (p /. j) by A1, A14, A15, A16; :: thesis: verum