let K be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being FinSequence of K
for i being Nat st i in dom p & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
Sum p = p . i
let p be FinSequence of K; :: thesis: for i being Nat st i in dom p & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
Sum p = p . i
let i be Nat; :: thesis: ( i in dom p & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) implies Sum p = p . i )
A1: i in NAT by ORDINAL1:def 13;
assume A2: ( i in dom p & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) ) ; :: thesis: Sum p = p . i
then reconsider a = p . i as Element of K by FINSEQ_2:13;
A3: ( 1 <= i & i <= len p ) by A2, FINSEQ_3:27;
A4: i <> 0 by A2, FINSEQ_3:27;
reconsider p1 = p | (Seg i) as FinSequence of K by FINSEQ_1:23;
p1 is_a_prefix_of p by A1, TREES_1:def 1;
then consider p2 being FinSequence such that
A5: p = p1 ^ p2 by TREES_1:8;
i in Seg i by A4, FINSEQ_1:5;
then i in (dom p) /\ (Seg i) by A2, XBOOLE_0:def 4;
then A6: i in dom p1 by RELAT_1:90;
then p1 <> {} ;
then len p1 <> 0 ;
then consider p3 being FinSequence of K, x being Element of K such that
A7: p1 = p3 ^ <*x*> by FINSEQ_2:22;
reconsider p2 = p2 as FinSequence of K by A5, FINSEQ_1:50;
A8: i = len p1 by A3, FINSEQ_1:21
.= (len p3) + (len <*x*>) by A7, FINSEQ_1:35
.= (len p3) + 1 by FINSEQ_1:56 ;
then A9: x = p1 . i by A7, FINSEQ_1:59
.= a by A5, A6, FINSEQ_1:def 7 ;
A10: for k being Nat st k in Seg (len p2) holds
p2 . k = 0. K

proof

let k be Nat; :: thesis: ( k in Seg (len p2) implies p2 . k = 0. K )
assume k in Seg (len p2) ; :: thesis: p2 . k = 0. K
then A11: k in dom p2 by FINSEQ_1:def 3;
A12: ( 1 <= i & i <= len p1 ) by A6, FINSEQ_3:27;
0 <> k by A11, FINSEQ_3:27;
then A13: len p1 <> (len p1) + k by XCMPLX_1:3;
len p1 <= (len p1) + k by NAT_1:12;
then A14: i <> (len p1) + k by A12, A13, XXREAL_0:1;
thus p2 . k = p . ((len p1) + k) by A5, A11, FINSEQ_1:def 7
.= 0. K by A2, A5, A11, A14, FINSEQ_1:41 ; :: thesis: verum

end;

A15: p2 = (len p2) |-> (0. K)

proof

A16: len ((len p2) |-> (0. K)) = len p2 by FINSEQ_1:def 18;
X: dom p2 = Seg (len p2) by FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom p2 implies p2 . j = ((len p2) |-> (0. K)) . j )
assume A17: j in dom p2 ; :: thesis: p2 . j = ((len p2) |-> (0. K)) . j
hence p2 . j = 0. K by A10, X
.= ((len p2) |-> (0. K)) . j by A17, X, FINSEQ_2:71 ;
:: thesis: verum

end;

hence p2 = (len p2) |-> (0. K) by A16, FINSEQ_2:10; :: thesis: verum

end;

A18: for k being Nat st k in Seg (len p3) holds
p3 . k = 0. K

proof

let k be Nat; :: thesis: ( k in Seg (len p3) implies p3 . k = 0. K )
assume A19: k in Seg (len p3) ; :: thesis: p3 . k = 0. K
then ( 1 <= k & k <= len p3 ) by FINSEQ_1:3;
then A20: i <> k by A8, NAT_1:13;
A21: k in dom p3 by A19, FINSEQ_1:def 3;
then A22: k in dom p1 by A7, FINSEQ_2:18;
thus p3 . k = p1 . k by A7, A21, FINSEQ_1:def 7
.= p . k by A5, A22, FINSEQ_1:def 7
.= 0. K by A2, A5, A20, A22, FINSEQ_2:18 ; :: thesis: verum

end;

A23: p3 = (len p3) |-> (0. K)

proof

A24: len ((len p3) |-> (0. K)) = len p3 by FINSEQ_1:def 18;
X: dom p3 = Seg (len p3) by FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom p3 implies p3 . j = ((len p3) |-> (0. K)) . j )
assume A25: j in dom p3 ; :: thesis: p3 . j = ((len p3) |-> (0. K)) . j
hence p3 . j = 0. K by A18, X
.= ((len p3) |-> (0. K)) . j by A25, X, FINSEQ_2:71 ;
:: thesis: verum

end;

hence p3 = (len p3) |-> (0. K) by A24, FINSEQ_2:10; :: thesis: verum

end;

Sum p = (Sum (p3 ^ <*x*>)) + (Sum ((len p2) |-> (0. K))) by A5, A7, A15, RLVECT_1:58
.= (Sum (p3 ^ <*x*>)) + (0. K) by Th13
.= Sum (p3 ^ <*x*>) by RLVECT_1:10
.= (Sum ((len p3) |-> (0. K))) + x by A23, FVSUM_1:87
.= (0. K) + a by A9, Th13
.= p . i by RLVECT_1:10 ;
hence Sum p = p . i ; :: thesis: verum