theorem Th54: :: ORDERS_5:45

for A being set
for D being a_partition of A
for f being finite-support Function of A,REAL holds D eqSumOf (- f) = - (D eqSumOf f)