let a, b, c be Element of 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)

c * (min a,b) = min (c * a),(c * b)

proof

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

end;

hence c * (min a,b) = min (c * a),(c * b) ; :: thesis: verum

end;

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

c * (min a,b) = min (c * a),(c * b)

proof

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

end;

hence c * (min a,b) = min (c * a),(c * b) ; :: thesis: verum

end;

end;