theorem Th3: :: RFUNCT_3:3

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