let r, s be real number ; :: thesis: ( 0 <= r implies max+ (r * s) = r * (max+ s) )
assume A1: 0 <= r ; :: thesis: max+ (r * s) = r * (max+ s)

now

per cases ( 0 <= s or s < 0 ) ;

case A2: 0 <= s ; :: thesis: max+ (r * s) = r * (max+ s)

then 0 <= r * s by A1;
then ( max+ (r * s) = r * s & r * (max+ s) = r * s ) by A2, XXREAL_0:def 10;
hence max+ (r * s) = r * (max+ s) ; :: thesis: verum

end;

case A3: s < 0 ; :: thesis: max+ (r * s) = r * (max+ s)

then A4: max+ s = 0 by XXREAL_0:def 10;
r * s <= 0 by A1, A3;
hence max+ (r * s) = r * (max+ s) by A4, XXREAL_0:def 10; :: thesis: verum

end;

end;

end;

hence max+ (r * s) = r * (max+ s) ; :: thesis: verum