for r being Real holds 2 * (max+ r) = r + |.r.|