:: deftheorem Def11 defines Sum EUCLID_7:def 11 :
for n being Nat
for f being FinSequence of REAL n holds
( ( len f > 0 implies Sum f = (accum f) . (len f) ) & ( not len f > 0 implies Sum f = 0* n ) );