let V be non empty addLoopStr ; :: thesis: for F being FinSequence of the carrier of V st len F = 0 holds
Sum F = 0. V
let F be FinSequence of the carrier 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