theorem Th4: :: RFUNCT_3:4

for r, s being Real st 0 <= r holds
max+ (r * s) = r * (max+ s)