let R be Ring; :: thesis: for V being LeftMod of R holds Sum (<*> the carrier of V) = 0. V
let V be LeftMod of R; :: thesis: Sum (<*> the carrier of V) = 0. V
set S = <*> the carrier of V;
ex f being sequence of V st
( Sum (<*> the carrier of V) = f . (len (<*> the carrier of V)) & f . 0 = 0. V & ( for j being Nat
for v being Vector of V st j < len (<*> the carrier of V) & v = (<*> the carrier of V) . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) by RLVECT_1:def 12;
hence Sum (<*> the carrier of V) = 0. V ; :: thesis: verum