let V be non empty addLoopStr ; :: 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 Element of V st j < len (<*> the carrier of V) & v = (<*> the carrier of V) . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) by Def12;
hence Sum (<*> the carrier of V) = 0. V ; :: thesis: verum