:: deftheorem defines Sum ZMODUL05:def 2 :
for T being finite Subset of the carrier of INT.Ring
for b₂ being Element of INT.Ring holds
( b₂ = Sum T iff ex F being FinSequence of INT st
( rng F = T & F is one-to-one & b₂ = Sum F ) );