let V be non empty addLoopStr ; :: thesis: for F being FinSequence-like PartFunc of NAT,V st len F = 0 holds
Sum F = 0. V
let F be FinSequence-like PartFunc of NAT,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 Lm4; :: thesis: verum