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 ;
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 ;
A9: i <= len p by ;
then A10: len (p | i) = i by FINSEQ_1:17;
A11: dom (p | i) = Seg i by ;
then not j in dom (p | i) by ;
then consider ji being Nat such that
A12: ji in dom q and
A13: j = i + ji by ;
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 ;
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
.= 0. K by ; :: thesis: verum
end;
then A18: Sum q = q . ji by
.= p . j by
.= p /. j by ;
A19: Seg i c= Seg (len p) by ;
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 ;
thus (p | i) . k = p . kk by
.= 0. K by A5, A6, A11, A19, A20, A21, A22 ; :: thesis: verum
end;
then Sum (p | i) = (p | i) . i by
.= p . i by
.= p /. i by ;
hence Sum p = (p /. i) + (p /. j) by ; :: 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 ;
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