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: S₁[ <*> the carrier of V1] by RLVECT_1:60;
A3: 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 A4: ( ( for k being Nat st k in dom p holds
p /. k = 0. V1 ) implies Sum p = 0. V1 ) ; :: thesis: S₁[p ^ <*x*>]
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

let k be Nat; :: thesis: ( k in dom p implies p /. k = 0. V1 )
assume A7: k in dom p ; :: thesis: p /. k = 0. V1
A8: dom p c= dom (p ^ <*x*>) by FINSEQ_1:39;
reconsider k1 = k as Element of NAT by ORDINAL1:def 13;
thus p /. k = p . k by A7, PARTFUN1:def 8
.= (p ^ <*x*>) . k1 by A7, FINSEQ_1:def 7
.= (p ^ <*x*>) /. k by A7, A8, PARTFUN1:def 8
.= 0. V1 by A5, A7, A8 ; :: thesis: verum

end;

A9: len (p ^ <*x*>) = (len p) + (len <*x*>) by FINSEQ_1:35
.= (len p) + 1 by FINSEQ_1:56 ;
(len p) + 1 in Seg ((len p) + 1) by FINSEQ_1:6;
then A10: (len p) + 1 in dom (p ^ <*x*>) by A9, FINSEQ_1:def 3;
A11: x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:59;
thus Sum (p ^ <*x*>) = (Sum p) + (Sum <*x*>) by RLVECT_1:58
.= (Sum p) + x by RLVECT_1:61
.= (Sum p) + ((p ^ <*x*>) /. ((len p) + 1)) by A10, A11, PARTFUN1:def 8
.= (0. V1) + (0. V1) by A4, A5, A6, A10
.= 0. V1 by RLVECT_1:def 7 ; :: thesis: verum

end;

for p being FinSequence of V1 holds S₁[p] from FINSEQ_2:sch 2(A2, A3);
hence Sum F = 0. V1 by A1; :: thesis: verum