let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being FinSequence of L st ( for i being Element of NAT st i in dom p holds
p . i = 0. L ) holds
Sum p = 0. L
let p be FinSequence of L; :: thesis: ( ( for i being Element of NAT st i in dom p holds
p . i = 0. L ) implies Sum p = 0. L )
assume A1: for k being Element of NAT st k in dom p holds
p . k = 0. L ; :: thesis: Sum p = 0. L
defpred S₁[ FinSequence of L] means ( ( for k being Element of NAT st k in dom $1 holds
$1 . k = 0. L ) implies Sum $1 = 0. L );
A2: for p being FinSequence of L
for x being Element of L st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of L; :: thesis: for x being Element of L st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of L; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A3: ( ( for k being Element of NAT st k in dom p holds
p . k = 0. L ) implies Sum p = 0. L ) ; :: thesis: S₁[p ^ <*x*>]
A4: (len p) + 1 in Seg ((len p) + 1) by FINSEQ_1:4;
assume A5: for k being Element of NAT st k in dom (p ^ <*x*>) holds
(p ^ <*x*>) . k = 0. L ; :: thesis: Sum (p ^ <*x*>) = 0. L
A6: for k being Element of NAT st k in dom p holds
p . k = 0. L

proof

A7: dom p c= dom (p ^ <*x*>) by FINSEQ_1:26;
let k be Element of NAT ; :: thesis: ( k in dom p implies p . k = 0. L )
assume A8: k in dom p ; :: thesis: p . k = 0. L
thus p . k = (p ^ <*x*>) . k by A8, FINSEQ_1:def 7
.= 0. L by A5, A8, A7 ; :: thesis: verum

end;

len (p ^ <*x*>) = (len p) + (len <*x*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:39 ;
then A9: (len p) + 1 in dom (p ^ <*x*>) by A4, FINSEQ_1:def 3;
A10: x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:42;
thus Sum (p ^ <*x*>) = (Sum p) + (Sum <*x*>) by RLVECT_1:41
.= (Sum p) + x by RLVECT_1:44
.= (0. L) + (0. L) by A3, A5, A6, A9, A10
.= 0. L by RLVECT_1:def 4 ; :: thesis: verum

end;

A11: S₁[ <*> the carrier of L] by RLVECT_1:43;
for p being FinSequence of L holds S₁[p] from FINSEQ_2:sch 2(A11, A2);
hence Sum p = 0. L by A1; :: thesis: verum