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: ( ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b₁ being ext-real number st b₁ = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b₁ being ext-real number st b₁ = -infty ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or 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 a + b ; :: thesis: ex a, b being complex number st
( x = a & y = b & a + b = a + b )
take a ; :: thesis: ex b being complex number st
( x = a & y = b & a + b = a + b )
take b ; :: thesis: ( x = a & y = b & a + b = a + b )
thus ( x = a & y = b & a + b = a + b ) ; :: thesis: verum

end;

thus ( ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b₁ being ext-real number st b₁ = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b₁ being ext-real number st b₁ = -infty ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ex b₁ being ext-real number st b₁ = 0 ) ) ; :: thesis: verum