let IT1, IT2 be Element of REAL ; :: thesis: ( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT1 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT2 = x9 + y9 ) implies IT1 = IT2 ) & ( x in REAL+ & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT1 = x9 - y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT2 = x9 - y9 ) implies IT1 = IT2 ) & ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT1 = y9 - x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT2 = y9 - x9 ) implies IT1 = IT2 ) & ( ( 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+:] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT2 = [0,(x9 + y9)] ) implies IT1 = IT2 ) )
thus ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT1 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT2 = x9 + y9 ) implies IT1 = IT2 ) ; :: thesis: ( ( x in REAL+ & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT1 = x9 - y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT2 = x9 - y9 ) implies IT1 = IT2 ) & ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT1 = y9 - x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT2 = y9 - x9 ) implies IT1 = IT2 ) & ( ( 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+:] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT2 = [0,(x9 + y9)] ) implies IT1 = IT2 ) )
thus ( x in REAL+ & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT1 = x9 - y9 ) & ex x99, y99 being Element of REAL+ st
( x = x99 & y = [0,y99] & IT2 = x99 - y99 ) implies IT1 = IT2 ) by XTUPLE_0:1; :: thesis: ( ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT1 = y9 - x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT2 = y9 - x9 ) implies IT1 = IT2 ) & ( ( 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+:] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT2 = [0,(x9 + y9)] ) implies IT1 = IT2 ) )
thus ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT1 = y9 - x9 ) & ex x99, y99 being Element of REAL+ st
( x = [0,x99] & y = y99 & IT2 = y99 - x99 ) implies IT1 = IT2 ) by XTUPLE_0:1; :: thesis: ( ( 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+:] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT2 = [0,(x9 + y9)] ) implies IT1 = IT2 )
assume that
( not x in REAL+ or not y in REAL+ ) and
( not x in REAL+ or not y in [:{0},REAL+:] ) and
( not y in REAL+ or not x in [:{0},REAL+:] ) ; :: thesis: ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not IT1 = [0,(x9 + y9)] ) or for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not IT2 = [0,(x9 + y9)] ) or IT1 = IT2 )
given x9, y9 being Element of REAL+ such that A18: x = [0,x9] and
A19: ( y = [0,y9] & IT1 = [0,(x9 + y9)] ) ; :: thesis: ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not IT2 = [0,(x9 + y9)] ) or IT1 = IT2 )
given x99, y99 being Element of REAL+ such that A20: x = [0,x99] and
A21: ( y = [0,y99] & IT2 = [0,(x99 + y99)] ) ; :: thesis: IT1 = IT2
x9 = x99 by A18, A20, XTUPLE_0:1;
hence IT1 = IT2 by A19, A21, XTUPLE_0:1; :: thesis: verum