for V1 being non empty right_complementable add-associative right_zeroed addLoopStr
for F being FinSequence of V1 st ( for k being Nat st k in dom F holds
F /. k = 0. V1 ) holds
Sum F = 0. V1