let a, b, c be Real; :: thesis: ( 0 <= c implies c * (max (a,b)) = max ((c * a),(c * b)) )
assume A1: 0 <= c ; :: thesis: c * (max (a,b)) = max ((c * a),(c * b))

per cases ( max (a,b) = b or max (a,b) = a ) by XXREAL_0:16;

suppose A2: max (a,b) = b ; :: thesis: c * (max (a,b)) = max ((c * a),(c * b))

then a <= b by XXREAL_0:def 10;
then a * c <= c * b by A1, XREAL_1:64;
hence c * (max (a,b)) = max ((c * a),(c * b)) by A2, XXREAL_0:def 10; :: thesis: verum

end;

suppose A3: max (a,b) = a ; :: thesis: c * (max (a,b)) = max ((c * a),(c * b))

then a >= b by XXREAL_0:def 10;
then a * c >= b * c by A1, XREAL_1:64;
hence c * (max (a,b)) = max ((c * a),(c * b)) by A3, XXREAL_0:def 10; :: thesis: verum

end;

end;