let x, y, k be ExtReal; :: thesis: ( 0 <= k implies ( k * (max (x,y)) = max ((k * x),(k * y)) & k * (min (x,y)) = min ((k * x),(k * y)) ) )

assume A1: 0 <= k ; :: thesis: ( k * (max (x,y)) = max ((k * x),(k * y)) & k * (min (x,y)) = min ((k * x),(k * y)) )

assume A1: 0 <= k ; :: thesis: ( k * (max (x,y)) = max ((k * x),(k * y)) & k * (min (x,y)) = min ((k * x),(k * y)) )

now :: thesis: k * (max (x,y)) = max ((k * x),(k * y))end;

hence
k * (max (x,y)) = max ((k * x),(k * y))
; :: thesis: k * (min (x,y)) = min ((k * x),(k * y))per cases
( max (x,y) = x or max (x,y) = y )
by XXREAL_0:16;

end;

per cases
( min (x,y) = x or min (x,y) = y )
by XXREAL_0:15;

end;