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

proof

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

proof

A7: dom p c= dom (p ^ <*x*>) by FINSEQ_1:26;
let k be Nat; :: thesis: ( k in dom p implies p /. k = 0. V1 )
assume A8: k in dom p ; :: thesis: p /. k = 0. V1
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
thus p /. k = p . k by A8, PARTFUN1:def 6
.= (p ^ <*x*>) . k1 by A8, FINSEQ_1:def 7
.= (p ^ <*x*>) /. k by A8, A7, PARTFUN1:def 6
.= 0. V1 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
.= (Sum p) + ((p ^ <*x*>) /. ((len p) + 1)) by A9, A10, PARTFUN1:def 6
.= (0. V1) + (0. V1) by A3, A5, A6, A9
.= 0. V1 by RLVECT_1:def 4 ; :: thesis: verum

end;

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