let V be non empty addLoopStr ; :: thesis: Sum (<*> the carrier of V) = 0. V
set S = <*> the carrier of V;
ex f being Function of NAT ,the carrier of V st
( Sum (<*> the carrier of V) = f . (len (<*> the carrier of V)) & f . 0 = 0. V & ( for j being Element of 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 Def13;
hence Sum (<*> the carrier of V) = 0. V ; :: thesis: verum