thus ( x is real & y is real implies ex c being ext-real number ex a, b being complex number st
( x = a & y = b & c = a * b ) ) :: thesis: ( ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ex b₁ being ext-real number st 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 ex b₁ being ext-real number st 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 ex b₁ being ext-real number st b₁ = 0 ) )

proof

assume ( x is real & y is real ) ; :: thesis: ex c being ext-real number ex a, b being complex number st
( x = a & y = b & c = a * b )
then reconsider a = x, b = y as real number ;
take c = a * b; :: thesis: ex a, b being complex number st
( x = a & y = b & c = a * b )
take a ; :: thesis: ex b being complex number st
( x = a & y = b & c = a * b )
take b ; :: thesis: ( x = a & y = b & c = a * b )
thus ( x = a & y = b & c = a * b ) ; :: thesis: 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 b₁ being ext-real number st 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 ex b₁ being ext-real number st 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 ex b₁ being ext-real number st b₁ = 0 ) ) ; :: thesis: verum