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 S1[ 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 S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of V1; :: thesis: for x being Element of V1 st S1[p] holds
S1[p ^ <*x*>]

let x be Element of V1; :: thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A3: ( ( for k being Nat st k in dom p holds
p /. k = 0. V1 ) implies Sum p = 0. V1 ) ; :: thesis: S1[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
.= (p ^ <*x*>) . k1 by
.= (p ^ <*x*>) /. k by
.= 0. V1 by A5, A8, A7 ; :: thesis: verum
end;
len (p ^ <*x*>) = (len p) + () by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:39 ;
then A9: (len p) + 1 in dom (p ^ <*x*>) by ;
A10: x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:42;
thus Sum (p ^ <*x*>) = (Sum p) + () by RLVECT_1:41
.= (Sum p) + x by RLVECT_1:44
.= (Sum p) + ((p ^ <*x*>) /. ((len p) + 1)) by
.= (0. V1) + (0. V1) by A3, A5, A6, A9
.= 0. V1 by RLVECT_1:def 4 ; :: thesis: verum
end;
A11: S1[ <*> the carrier of V1] by RLVECT_1:43;
for p being FinSequence of V1 holds S1[p] from hence Sum F = 0. V1 by A1; :: thesis: verum