let x, y, k be ExtReal; ( 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
; ( k * (max (x,y)) = max ((k * x),(k * y)) & k * (min (x,y)) = min ((k * x),(k * y)) )
hence
k * (max (x,y)) = max ((k * x),(k * y))
; k * (min (x,y)) = min ((k * x),(k * y))