let x, y be R_eal; :: thesis: ( - (x * y) = x * (- y) & - (x * y) = (- x) * y )

now

per cases ( ex a, b being Real st
( x = a & y = b & x * y = a * b ) or ( ( ( 0. < x & y = +infty ) or ( 0. < y & x = +infty ) or ( x < 0. & y = -infty ) or ( y < 0. & x = -infty ) ) & x * y = +infty ) or ( ( ( x < 0. & y = +infty ) or ( y < 0. & x = +infty ) or ( 0. < x & y = -infty ) or ( 0. < y & x = -infty ) ) & x * y = -infty ) or ( ( x = 0. or y = 0. ) & x * y = 0. ) ) by Def1;

suppose ex a, b being Real st
( x = a & y = b & x * y = a * b ) ; :: thesis: ( - (x * y) = x * (- y) & - (x * y) = (- x) * y )

then consider a, b being Real such that
A1: ( x = a & y = b & x * y = a * b ) ;
A2: ( - x = - a & - y = - b & - (x * y) = - (a * b) ) by A1, SUPINF_2:3;
then ( x * (- y) = a * (- b) & (- x) * y = (- a) * b ) by A1, Th13;
hence ( - (x * y) = x * (- y) & - (x * y) = (- x) * y ) by A2; :: thesis: verum

end;

suppose A3: ( ( ( 0. < x & y = +infty ) or ( 0. < y & x = +infty ) or ( x < 0. & y = -infty ) or ( y < 0. & x = -infty ) ) & x * y = +infty ) ; :: thesis: ( - (x * y) = x * (- y) & - (x * y) = (- x) * y )

then A4: - (x * y) = -infty by Th4;
A5: ( ( - x < 0. & y = +infty ) or ( 0. < y & - x = -infty ) or ( 0. < - x & y = -infty ) or ( y < 0. & - x = +infty ) ) by A3, Th4, Th24, SUPINF_2:17;
( ( 0. < x & - y = -infty ) or ( - y < 0. & x = +infty ) or ( x < 0. & - y = +infty ) or ( 0. < - y & x = -infty ) ) by A3, Th4, Th24, SUPINF_2:17;
hence ( - (x * y) = x * (- y) & - (x * y) = (- x) * y ) by A4, A5, Def1; :: thesis: verum

end;

suppose A6: ( ( ( x < 0. & y = +infty ) or ( y < 0. & x = +infty ) or ( 0. < x & y = -infty ) or ( 0. < y & x = -infty ) ) & x * y = -infty ) ; :: thesis: ( - (x * y) = x * (- y) & - (x * y) = (- x) * y )

then A7: - (x * y) = +infty by Th4;
A8: ( ( 0. < - x & y = +infty ) or ( y < 0. & - x = -infty ) or ( - x < 0. & y = -infty ) or ( 0. < y & - x = +infty ) ) by A6, Th4, Th24, SUPINF_2:17;
( ( x < 0. & - y = -infty ) or ( 0. < - y & x = +infty ) or ( 0. < x & - y = +infty ) or ( - y < 0. & x = -infty ) ) by A6, Th4, Th24, SUPINF_2:17;
hence ( - (x * y) = x * (- y) & - (x * y) = (- x) * y ) by A7, A8, Def1; :: thesis: verum

end;

suppose ( ( x = 0. or y = 0. ) & x * y = 0. ) ; :: thesis: ( - (x * y) = x * (- y) & - (x * y) = (- x) * y )

hence ( - (x * y) = x * (- y) & - (x * y) = (- x) * y ) by Def1, Th24; :: thesis: verum

end;

end;

end;

hence ( - (x * y) = x * (- y) & - (x * y) = (- x) * y ) ; :: thesis: verum