theorem lembag2b: :: FIELD_14:1

for f being FinSequence of NAT
for i, j being Nat st i in dom f & j in dom f & i <> j holds
Sum f >= (f . i) + (f . j)