thus
( x is real & y is real implies ex c being ExtReal ex a, b being Complex st
( x = a & y = b & c = 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 ex b1 being ExtReal st b1 = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ex b1 being ExtReal st b1 = -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 ex b1 being ExtReal st b1 = 0 ) )proof
assume
(
x is
real &
y is
real )
;
ex c being ExtReal ex a, b being Complex st
( x = a & y = b & c = a * b )
then reconsider a =
x,
b =
y as
Real ;
take
a * b
;
ex a, b being Complex st
( x = a & y = b & a * b = a * b )
take
a
;
ex b being Complex st
( x = a & y = b & a * b = a * b )
take
b
;
( x = a & y = b & a * b = a * b )
thus
(
x = a &
y = b &
a * b = a * b )
;
verum
end;
thus
( ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ex b1 being ExtReal st b1 = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ex b1 being ExtReal st b1 = -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 ex b1 being ExtReal st b1 = 0 ) )
; verum