let R be Ring; :: thesis: for V being LeftMod of R
for F being FinSequence of V st len F = 0 holds
Sum F = 0. V
let V be LeftMod of R; :: thesis: for F being FinSequence of V st len F = 0 holds
Sum F = 0. V
let F be FinSequence of V; :: thesis: ( len F = 0 implies Sum F = 0. V )
assume len F = 0 ; :: thesis: Sum F = 0. V
then F = <*> the carrier of V ;
hence Sum F = 0. V by Lm1; :: thesis: verum