hereby ( ( x in REAL+ & y in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b1 = x9 - y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) ) )
end;
A1:
y in REAL+ \/ [:{0},REAL+:]
by XBOOLE_0:def 5;
hereby ( ( y in REAL+ & x in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) ) )
assume
x in REAL+
;
( y in [:{0},REAL+:] implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = x9 - y9 ) )then reconsider x9 =
x as
Element of
REAL+ ;
assume
y in [:{0},REAL+:]
;
ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = x9 - y9 )then consider z,
y9 being
object such that A2:
z in {0}
and A3:
y9 in REAL+
and A4:
y = [z,y9]
by ZFMISC_1:84;
reconsider y9 =
y9 as
Element of
REAL+ by A3;
reconsider IT =
x9 - y9 as
Element of
REAL by Th4;
take IT =
IT;
ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = x9 - y9 )take x9 =
x9;
ex y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = x9 - y9 )take y9 =
y9;
( x = x9 & y = [0,y9] & IT = x9 - y9 )thus
(
x = x9 &
y = [0,y9] &
IT = x9 - y9 )
by A2, A4, TARSKI:def 1;
verum
end;
hereby ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) )
assume
y in REAL+
;
( x in [:{0},REAL+:] implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = y9 - x9 ) )then reconsider y9 =
y as
Element of
REAL+ ;
assume
x in [:{0},REAL+:]
;
ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = y9 - x9 )then consider z,
x9 being
object such that A5:
z in {0}
and A6:
x9 in REAL+
and A7:
x = [z,x9]
by ZFMISC_1:84;
reconsider x9 =
x9 as
Element of
REAL+ by A6;
reconsider IT =
y9 - x9 as
Element of
REAL by Th4;
take IT =
IT;
ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = y9 - x9 )take x9 =
x9;
ex y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = y9 - x9 )take y9 =
y9;
( x = [0,x9] & y = y9 & IT = y9 - x9 )thus
(
x = [0,x9] &
y = y9 &
IT = y9 - x9 )
by A5, A7, TARSKI:def 1;
verum
end;
assume that
A8:
( not x in REAL+ or not y in REAL+ )
and
A9:
( not x in REAL+ or not y in [:{0},REAL+:] )
and
A10:
( not y in REAL+ or not x in [:{0},REAL+:] )
; ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] )
A11:
x in REAL+ \/ [:{0},REAL+:]
by XBOOLE_0:def 5;
then
( x in REAL+ or x in [:{0},REAL+:] )
by XBOOLE_0:def 3;
then consider z1, x9 being object such that
A12:
z1 in {0}
and
A13:
x9 in REAL+
and
A14:
x = [z1,x9]
by A1, A8, A9, XBOOLE_0:def 3, ZFMISC_1:84;
( y in REAL+ or y in [:{0},REAL+:] )
by A1, XBOOLE_0:def 3;
then consider z2, y9 being object such that
A15:
z2 in {0}
and
A16:
y9 in REAL+
and
A17:
y = [z2,y9]
by A11, A8, A10, XBOOLE_0:def 3, ZFMISC_1:84;
reconsider x9 = x9 as Element of REAL+ by A13;
reconsider y9 = y9 as Element of REAL+ by A16;
x = [0,x9]
by A12, A14, TARSKI:def 1;
then
x9 + y9 <> 0
by Th3, ARYTM_2:5;
then reconsider IT = [0,(y9 + x9)] as Element of REAL by Th2;
take
IT
; ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT = [0,(x9 + y9)] )
take
x9
; ex y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT = [0,(x9 + y9)] )
take
y9
; ( x = [0,x9] & y = [0,y9] & IT = [0,(x9 + y9)] )
thus
( x = [0,x9] & y = [0,y9] & IT = [0,(x9 + y9)] )
by A12, A14, A15, A17, TARSKI:def 1; verum