let x, y, k be ext-real number ; :: 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) )

now

per cases ( max x,y = x or max x,y = y ) by XXREAL_0:16;

suppose A2: max x,y = x ; :: thesis: k * (max x,y) = max (k * x),(k * y)

then y <= x by XXREAL_0:def 10;
then k * y <= k * x by A1, XXREAL_3:82;
hence k * (max x,y) = max (k * x),(k * y) by A2, XXREAL_0:def 10; :: thesis: verum

end;

suppose A3: max x,y = y ; :: thesis: k * (max x,y) = max (k * x),(k * y)

then x <= y by XXREAL_0:def 10;
then k * x <= k * y by A1, XXREAL_3:82;
hence k * (max x,y) = max (k * x),(k * y) by A3, XXREAL_0:def 10; :: thesis: verum

end;

end;

end;

hence k * (max x,y) = max (k * x),(k * y) ; :: thesis: k * (min x,y) = min (k * x),(k * y)

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

suppose A4: min x,y = x ; :: thesis: k * (min x,y) = min (k * x),(k * y)

then x <= y by XXREAL_0:def 9;
then k * x <= k * y by A1, XXREAL_3:82;
hence k * (min x,y) = min (k * x),(k * y) by A4, XXREAL_0:def 9; :: thesis: verum

end;

suppose A5: min x,y = y ; :: thesis: k * (min x,y) = min (k * x),(k * y)

then y <= x by XXREAL_0:def 9;
then k * y <= k * x by A1, XXREAL_3:82;
hence k * (min x,y) = min (k * x),(k * y) by A5, XXREAL_0:def 9; :: thesis: verum

end;

end;