:: deftheorem Def5 defines * XXREAL_3:def 5 :
for x, y, b₃ being ExtReal holds
( ( x is real & y is real implies ( b₃ = x * y iff ex a, b being Complex st
( x = a & y = b & b₃ = a * b ) ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ( b₃ = x * y iff b₃ = +infty ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( b₃ = x * y iff b₃ = -infty ) ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies ( b₃ = x * y iff b₃ = 0 ) ) );