let K be non empty right_complementable add-associative right_zeroed addLoopStr ; 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; 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; ( 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
; 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;
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;
( 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)
;
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
;
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;
( k in Seg (len p3) implies p3 . k = 0. K )
assume A17:
k in Seg (len p3)
;
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
;
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 Th11
.=
Sum (p3 ^ <*x*>)
by RLVECT_1:4
.=
(Sum ((len p3) |-> (0. K))) + x
by A23, FVSUM_1:71
.=
(0. K) + a
by A15, Th11
.=
p . i
by RLVECT_1:4
;
hence
Sum p = p . i
; verum