for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX
for D being Division of A
for F being middle_volume of f,D
for Fr being middle_volume of Re f,D st Fr = Re F holds
Re (middle_sum (f,F)) = middle_sum ((Re f),Fr) by Th7;