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