let x, y, z be Element of REAL ; :: thesis: ( + (x,y) = 0 & + (x,z) = 0 implies y = z )
assume that
A1: + (x,y) = 0 and
A2: + (x,z) = 0 ; :: thesis: y = z
per cases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & y in REAL+ & z in ) or ( x in REAL+ & z in REAL+ & y in ) or ( x in REAL+ & y in & z in ) or ( z in REAL+ & y in REAL+ & x in ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in ) & ( not y in REAL+ or not x in ) ) or ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in ) & ( not z in REAL+ or not x in ) ) ) ;
suppose ( x in REAL+ & y in REAL+ & z in REAL+ ) ; :: thesis: y = z
then ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & z = y9 & 0 = x9 + y9 ) ) by ;
hence y = z by ARYTM_2:11; :: thesis: verum
end;
suppose that A3: x in REAL+ and
A4: y in REAL+ and
A5: z in ; :: thesis: y = z
A6: ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 ) by ;
consider x99, y99 being Element of REAL+ such that
A7: x = x99 and
A8: ( z = [0,y99] & 0 = x99 - y99 ) by ;
A9: x99 = 0 by ;
[{},{}] in by TARSKI:def 1;
then A10: not [{},{}] in REAL by ;
z in REAL ;
hence y = z by ; :: thesis: verum
end;
suppose that A11: x in REAL+ and
A12: z in REAL+ and
A13: y in ; :: thesis: y = z
A14: ex x9, z9 being Element of REAL+ st
( x = x9 & z = z9 & 0 = x9 + z9 ) by ;
consider x99, y9 being Element of REAL+ such that
A15: x = x99 and
A16: ( y = [0,y9] & 0 = x99 - y9 ) by ;
A17: x99 = 0 by ;
[0,0] in by TARSKI:def 1;
then A18: not [0,0] in REAL by ;
y in REAL ;
hence y = z by ; :: thesis: verum
end;
suppose that A19: x in REAL+ and
A20: y in and
A21: z in ; :: thesis: y = z
consider x9, y9 being Element of REAL+ such that
A22: x = x9 and
A23: y = [0,y9] and
A24: 0 = x9 - y9 by ;
consider x99, z9 being Element of REAL+ such that
A25: x = x99 and
A26: z = [0,z9] and
A27: 0 = x99 - z9 by ;
y9 = x9 by
.= z9 by ;
hence y = z by ; :: thesis: verum
end;
suppose that A28: z in REAL+ and
A29: y in REAL+ and
A30: x in ; :: thesis: y = z
consider x9, y9 being Element of REAL+ such that
A31: x = [0,x9] and
A32: y = y9 and
A33: 0 = y9 - x9 by ;
consider x99, z9 being Element of REAL+ such that
A34: x = [0,x99] and
A35: z = z9 and
A36: 0 = z9 - x99 by ;
x9 = x99 by ;
then z9 = x9 by
.= y9 by ;
hence y = z by ; :: thesis: verum
end;
suppose ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in ) & ( not y in REAL+ or not x in ) ) ; :: thesis: y = z
then ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & 0 = [0,(x9 + y9)] ) by ;
hence y = z ; :: thesis: verum
end;
suppose ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in ) & ( not z in REAL+ or not x in ) ) ; :: thesis: y = z
then ex x9, z9 being Element of REAL+ st
( x = [0,x9] & z = [0,z9] & 0 = [0,(x9 + z9)] ) by ;
hence y = z ; :: thesis: verum
end;
end;