let x, y, z be ExtReal; ( z is real implies (z + x) - (z + y) = x - y )
assume A1:
z is real
; (z + x) - (z + y) = x - y
per cases
( x = -infty or y = +infty or ( x in REAL & y in REAL & z in REAL ) or ( x = +infty & y in REAL & z in REAL ) or ( x in REAL & y = -infty & z in REAL ) or ( x = +infty & y = -infty & z in REAL ) )
by A1, XXREAL_0:14;
suppose A8:
y = +infty
;
(z + x) - (z + y) = x - yper cases
( x = -infty or x = +infty or x in REAL )
by XXREAL_0:14;
suppose A11:
x in REAL
;
(z + x) - (z + y) = x - ythen consider a,
b being
Complex such that A12:
(
z = a &
x = b )
and
z + x = a + b
by A1, Def2;
reconsider a =
a,
b =
b as
Real by A1, A11, A12;
A13:
a + b in REAL
by XREAL_0:def 1;
A14:
- +infty = -infty
by Def3;
(z + x) - (z + +infty) =
(z + x) - +infty
by A1, Def2
.=
(z + x) + -infty
by Def3
.=
-infty
by A12, A13, Def2
.=
x + (- +infty)
by A11, A14, Def2
;
hence
(z + x) - (z + y) = x - y
by A8;
verum end; end; end; end;