let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being FinSequence of the carrier 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 the carrier 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

now :: thesis: for k being Nat st k in dom p holds
p /. k = 0. L

let k be Nat; :: thesis: ( k in dom p implies p /. k = 0. L )
assume A2: k in dom p ; :: thesis: p /. k = 0. L
hence p /. k = p . k by PARTFUN1:def 6
.= 0. L by A1, A2 ;
:: thesis: verum

end;

hence Sum p = 0. L by MATRLIN:11; :: thesis: verum