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

per cases ( min (a,b) = a or min (a,b) = b ) by XXREAL_0:15;

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

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

end;

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

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

end;

end;