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 )
assume that
A1: i in dom p and
A2: for k being Nat st k in dom p & k <> i holds
p . k = 0. K ; :: thesis: Sum p = p . i
reconsider a = p . i as Element of K by A1, FINSEQ_2:11;
reconsider p1 = p | (Seg i) as FinSequence of K by FINSEQ_1:18;
i <> 0 by A1, FINSEQ_3:25;
then i in Seg i by FINSEQ_1:3;
then i in (dom p) /\ (Seg i) by A1, XBOOLE_0:def 4;
then A3: i in dom p1 by RELAT_1:61;
then p1 <> {} ;
then len p1 <> 0 ;
then consider p3 being FinSequence of K, x being Element of K such that
A4: p1 = p3 ^ <*x*> by FINSEQ_2:19;
i in NAT by ORDINAL1:def 12;
then p1 is_a_prefix_of p by TREES_1:def 1;
then consider p2 being FinSequence such that
A5: p = p1 ^ p2 by TREES_1:1;
reconsider p2 = p2 as FinSequence of K by A5, FINSEQ_1:36;
A6: dom p2 = Seg (len p2) by FINSEQ_1:def 3;
A7: 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 )
A8: ( i <= len p1 & len p1 <= (len p1) + k ) by A3, FINSEQ_3:25, NAT_1:12;
assume k in Seg (len p2) ; :: thesis: p2 . k = 0. K
then A9: k in dom p2 by FINSEQ_1:def 3;
then 0 <> k by FINSEQ_3:25;
then A10: i <> (len p1) + k by A8, XCMPLX_1:3, XXREAL_0:1;
thus p2 . k = p . ((len p1) + k) by A5, A9, FINSEQ_1:def 7
.= 0. K by A2, A5, A9, A10, FINSEQ_1:28 ; :: thesis: verum

end;

A11: now

let j be Nat; :: thesis: ( j in dom p2 implies p2 . j = ((len p2) |-> (0. K)) . j )
assume A12: j in dom p2 ; :: thesis: p2 . j = ((len p2) |-> (0. K)) . j
hence p2 . j = 0. K by A7, A6
.= ((len p2) |-> (0. K)) . j by A6, A12, FINSEQ_2:57 ;
:: thesis: verum

end;

A13: dom p3 = Seg (len p3) by FINSEQ_1:def 3;
i <= len p by A1, FINSEQ_3:25;
then A14: i = len p1 by FINSEQ_1:17
.= (len p3) + (len <*x*>) by A4, FINSEQ_1:22
.= (len p3) + 1 by FINSEQ_1:39 ;
then A15: x = p1 . i by A4, FINSEQ_1:42
.= a by A5, A3, FINSEQ_1:def 7 ;
A16: 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 A17: k in Seg (len p3) ; :: thesis: p3 . k = 0. K
then k <= len p3 by FINSEQ_1:1;
then A18: i <> k by A14, NAT_1:13;
A19: k in dom p3 by A17, FINSEQ_1:def 3;
then A20: k in dom p1 by A4, FINSEQ_2:15;
thus p3 . k = p1 . k by A4, A19, FINSEQ_1:def 7
.= p . k by A5, A20, FINSEQ_1:def 7
.= 0. K by A2, A5, A18, A20, FINSEQ_2:15 ; :: thesis: verum

end;

A21: now

let j be Nat; :: thesis: ( j in dom p3 implies p3 . j = ((len p3) |-> (0. K)) . j )
assume A22: j in dom p3 ; :: thesis: p3 . j = ((len p3) |-> (0. K)) . j
hence p3 . j = 0. K by A16, A13
.= ((len p3) |-> (0. K)) . j by A13, A22, FINSEQ_2:57 ;
:: thesis: verum

end;

len ((len p3) |-> (0. K)) = len p3 by CARD_1:def 7;
then A23: p3 = (len p3) |-> (0. K) by A21, FINSEQ_2:9;
len ((len p2) |-> (0. K)) = len p2 by CARD_1:def 7;
then p2 = (len p2) |-> (0. K) by A11, FINSEQ_2:9;
then Sum p = (Sum (p3 ^ <*x*>)) + (Sum ((len p2) |-> (0. K))) by A5, A4, RLVECT_1:41
.= (Sum (p3 ^ <*x*>)) + (0. K) by Th13
.= Sum (p3 ^ <*x*>) by RLVECT_1:4
.= (Sum ((len p3) |-> (0. K))) + x by A23, FVSUM_1:71
.= (0. K) + a by A15, Th13
.= p . i by RLVECT_1:4 ;
hence Sum p = p . i ; :: thesis: verum