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

now :: thesis: ( ( 0 <= s & max+ (r * s) = r * (max+ s) ) or ( s < 0 & max+ (r * s) = r * (max+ s) ) )

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

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

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

end;

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

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

end;

end;

end;

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