let a, b, c be Element of 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:66;
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:66;
hence c * (max a,b) = max (c * a),(c * b) by A3, XXREAL_0:def 10; :: thesis: verum

end;

end;