for a being Complex holds (a / 2) + (a / 2) = a ;