let z be R_eal; :: thesis: ( ( x in REAL & y in REAL implies ( z = x + y iff ex a, b being Real st
( x = a & y = b & z = a + b ) ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( z = x + y iff z = +infty ) ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( z = x + y iff z = -infty ) ) & ( ( x in REAL & y in REAL ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ( z = x + y iff z = 0. ) ) )
thus ( x in REAL & y in REAL implies ( z = x + y iff ex a, b being Real st
( x = a & y = b & z = a + b ) ) ) :: thesis: ( ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( z = x + y iff z = +infty ) ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( z = x + y iff z = -infty ) ) & ( ( x in REAL & y in REAL ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ( z = x + y iff z = 0. ) ) )

proof

assume Z: ( x in REAL & y in REAL ) ; :: thesis: ( z = x + y iff ex a, b being Real st
( x = a & y = b & z = a + b ) )
thus ( z = x + y implies ex a, b being Real st
( x = a & y = b & z = a + b ) ) :: thesis: ( ex a, b being Real st
( x = a & y = b & z = a + b ) implies z = x + y )

proof

assume ZZ: z = x + y ; :: thesis: ex a, b being Real st
( x = a & y = b & z = a + b )
reconsider x = x, y = y as Real by Z;
take x ; :: thesis: ex b being Real st
( x = x & y = b & z = x + b )
take y ; :: thesis: ( x = x & y = y & z = x + y )
thus ( x = x & y = y & z = x + y ) by ZZ, XXREAL_3:def 1; :: thesis: verum

end;

thus ( ex a, b being Real st
( x = a & y = b & z = a + b ) implies z = x + y ) by XXREAL_3:def 1; :: thesis: verum

end;

thus ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( z = x + y iff z = +infty ) ) by XXREAL_3:def 1; :: thesis: ( ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( z = x + y iff z = -infty ) ) & ( ( x in REAL & y in REAL ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ( z = x + y iff z = 0. ) ) )
thus ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( z = x + y iff z = -infty ) ) by XXREAL_3:def 1; :: thesis: ( ( x in REAL & y in REAL ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ( z = x + y iff z = 0. ) )
assume ( ( not x in REAL or not y in REAL ) & not ( x = +infty & y <> -infty ) & not ( y = +infty & x <> -infty ) & not ( x = -infty & y <> +infty ) & not ( y = -infty & x <> +infty ) ) ; :: thesis: ( z = x + y iff z = 0. )
then ( ( x = +infty & y = -infty ) or ( y = +infty & x = -infty ) ) by XXREAL_0:14;
hence ( z = x + y iff z = 0 ) by XXREAL_3:def 1; :: thesis: verum