let x, y, z be Element of REAL ; :: thesis:
A1: ( x in REAL+ \/ [:{0 },REAL+ :] & y in REAL+ \/ [:{0 },REAL+ :] ) by NUMBERS:def 1, XBOOLE_0:def 5;
A2: z in REAL+ \/ [:{0 },REAL+ :] by NUMBERS:def 1, XBOOLE_0:def 5;

per cases by A1, A2, XBOOLE_0:def 3;

suppose that A3: x in REAL+ and
A4: y in REAL+ and
A5: z in REAL+ ; :: thesis:

A6: ex x'', y'' being Element of REAL+ st
( x = x'' & y = y'' & + x,y = x'' + y'' ) by A3, A4, Def2;
then A7: ex xy'', z'' being Element of REAL+ st
( + x,y = xy'' & z = z'' & + (+ x,y),z = xy'' + z'' ) by A5, Def2;
A8: ex y', z' being Element of REAL+ st
( y = y' & z = z' & + y,z = y' + z' ) by A4, A5, Def2;
then ex x', yz' being Element of REAL+ st
( x = x' & + y,z = yz' & + x,(+ y,z) = x' + yz' ) by A3, Def2;
hence + x,(+ y,z) = + (+ x,y),z by A8, A6, A7, ARYTM_2:7; :: thesis:

end;

suppose that A9: x in REAL+ and
A10: y in REAL+ and
A11: z in [:{0 },REAL+ :] ; :: thesis:

A12: ex x'', y'' being Element of REAL+ st
( x = x'' & y = y'' & + x,y = x'' + y'' ) by A9, A10, Def2;
then consider xy'', z'' being Element of REAL+ such that
A13: + x,y = xy'' and
A14: z = [0 ,z''] and
A15: + (+ x,y),z = xy'' - z'' by A11, Def2;
consider y', z' being Element of REAL+ such that
A16: y = y' and
A17: z = [0 ,z'] and
A18: + y,z = y' - z' by A10, A11, Def2;
A19: z' = z'' by A17, A14, ZFMISC_1:33;

now

per cases ;

suppose A20: z' <=' y' ; :: thesis:

then A21: + y,z = y' -' z' by A18, ARYTM_1:def 2;
then ex x', yz' being Element of REAL+ st
( x = x' & + y,z = yz' & + x,(+ y,z) = x' + yz' ) by A9, Def2;
hence + x,(+ y,z) = + (+ x,y),z by A16, A12, A13, A15, A19, A20, A21, ARYTM_1:20; :: thesis:

end;

suppose A22: not z' <=' y' ; :: thesis:

then A23: + y,z = [0 ,(z' -' y')] by A18, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A24: x = x' and
A25: ( + y,z = [0 ,yz'] & + x,(+ y,z) = x' - yz' ) by A9, Def2;
thus + x,(+ y,z) = x' - (z' -' y') by A23, A25, ZFMISC_1:33
.= + (+ x,y),z by A16, A12, A13, A15, A19, A22, A24, ARYTM_1:21 ; :: thesis:

end;

hence + x,(+ y,z) = + (+ x,y),z ; :: thesis:

end;

suppose that A26: x in REAL+ and
A27: y in [:{0 },REAL+ :] and
A28: z in REAL+ ; :: thesis:

consider x'', y'' being Element of REAL+ such that
A29: x = x'' and
A30: y = [0 ,y''] and
A31: + x,y = x'' - y'' by A26, A27, Def2;
consider z', y' being Element of REAL+ such that
A32: z = z' and
A33: y = [0 ,y'] and
A34: + y,z = z' - y' by A27, A28, Def2;
A35: y' = y'' by A33, A30, ZFMISC_1:33;

now

per cases ;

suppose that A36: y' <=' x'' and
A37: y' <=' z' ; :: thesis:

A38: + y,z = z' -' y' by A34, A37, ARYTM_1:def 2;
then consider x', yz' being Element of REAL+ such that
A39: x = x' and
A40: ( + y,z = yz' & + x,(+ y,z) = x' + yz' ) by A26, Def2;
A41: + x,y = x' -' y' by A29, A31, A35, A36, A39, ARYTM_1:def 2;
then ex z'', xy'' being Element of REAL+ st
( z = z'' & + x,y = xy'' & + z,(+ x,y) = z'' + xy'' ) by A28, Def2;
hence + x,(+ y,z) = + (+ x,y),z by A32, A29, A36, A37, A38, A39, A40, A41, ARYTM_1:12; :: thesis:

end;

suppose that A42: y' <=' x'' and
A43: not y' <=' z' ; :: thesis:

A44: + x,y = x'' -' y' by A31, A35, A42, ARYTM_1:def 2;
then A45: ex z'', xy'' being Element of REAL+ st
( z = z'' & + x,y = xy'' & + z,(+ x,y) = z'' + xy'' ) by A28, Def2;
A46: + y,z = [0 ,(y' -' z')] by A34, A43, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A47: x = x' and
A48: ( + y,z = [0 ,yz'] & + x,(+ y,z) = x' - yz' ) by A26, Def2;
thus + x,(+ y,z) = x' - (y' -' z') by A46, A48, ZFMISC_1:33
.= + (+ x,y),z by A32, A29, A42, A43, A47, A44, A45, ARYTM_1:22 ; :: thesis:

end;

suppose that A49: not y' <=' x'' and
A50: y' <=' z' ; :: thesis:

A51: + y,x = [0 ,(y' -' x'')] by A31, A35, A49, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider z'', yx'' being Element of REAL+ such that
A52: z = z'' and
A53: ( + y,x = [0 ,yx''] & + z,(+ y,x) = z'' - yx'' ) by A28, Def2;
A54: + z,y = z' -' y' by A34, A50, ARYTM_1:def 2;
then ex x', zy'' being Element of REAL+ st
( x = x' & + z,y = zy'' & + x,(+ z,y) = x' + zy'' ) by A26, Def2;
hence + x,(+ y,z) = z'' - (y' -' x'') by A32, A29, A49, A50, A52, A54, ARYTM_1:22
.= + (+ x,y),z by A51, A53, ZFMISC_1:33 ;
:: thesis:

end;

suppose that A55: not y' <=' x'' and
A56: not y' <=' z' ; :: thesis:

A57: + y,z = [0 ,(y' -' z')] by A34, A56, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A58: x = x' and
A59: ( + y,z = [0 ,yz'] & + x,(+ y,z) = x' - yz' ) by A26, Def2;
A60: + y,x = [0 ,(y' -' x'')] by A31, A35, A55, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider z'', yx'' being Element of REAL+ such that
A61: z = z'' and
A62: ( + y,x = [0 ,yx''] & + z,(+ y,x) = z'' - yx'' ) by A28, Def2;
thus + x,(+ y,z) = x' - (y' -' z') by A57, A59, ZFMISC_1:33
.= z'' - (y' -' x'') by A32, A29, A55, A56, A61, A58, ARYTM_1:23
.= + (+ x,y),z by A60, A62, ZFMISC_1:33 ; :: thesis:

end;

hence + x,(+ y,z) = + (+ x,y),z ; :: thesis:

end;

suppose that A63: x in REAL+ and
A64: y in [:{0 },REAL+ :] and
A65: z in [:{0 },REAL+ :] ; :: thesis:

( ( not z in REAL+ or not y in [:{0 },REAL+ :] ) & ( not y in REAL+ or not z in [:{0 },REAL+ :] ) ) by A64, A65, Th5, XBOOLE_0:3;
then consider y', z' being Element of REAL+ such that
A66: y = [0 ,y'] and
A67: z = [0 ,z'] and
A68: + y,z = [0 ,(y' + z')] by A64, Def2;
+ y,z in [:{0 },REAL+ :] by A68, Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A69: x = x' and
A70: + y,z = [0 ,yz'] and
A71: + x,(+ y,z) = x' - yz' by A63, Def2;
consider x'', y'' being Element of REAL+ such that
A72: x = x'' and
A73: y = [0 ,y''] and
A74: + x,y = x'' - y'' by A63, A64, Def2;
A75: y' = y'' by A66, A73, ZFMISC_1:33;

now

per cases ;

suppose A76: y'' <=' x'' ; :: thesis:

then A77: + x,y = x'' -' y'' by A74, ARYTM_1:def 2;
then consider xy'', z'' being Element of REAL+ such that
A78: + x,y = xy'' and
A79: z = [0 ,z''] and
A80: + (+ x,y),z = xy'' - z'' by A65, Def2;
A81: z' = z'' by A67, A79, ZFMISC_1:33;
thus + x,(+ y,z) = x' - (y' + z') by A68, A70, A71, ZFMISC_1:33
.= + (+ x,y),z by A72, A69, A75, A76, A77, A78, A80, A81, ARYTM_1:24 ; :: thesis:

end;

suppose A82: not y'' <=' x'' ; :: thesis:

A83: ( not z in REAL+ or not + x,y in [:{0 },REAL+ :] ) by A65, Th5, XBOOLE_0:3;
A84: + x,y = [0 ,(y'' -' x'')] by A74, A82, ARYTM_1:def 2;
then + x,y in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( not + x,y in REAL+ or not z in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider xy'', z'' being Element of REAL+ such that
A85: + x,y = [0 ,xy''] and
A86: z = [0 ,z''] and
A87: + (+ x,y),z = [0 ,(xy'' + z'')] by A84, A83, Def2, Lm1, ZFMISC_1:106;
A88: z' = z'' by A67, A86, ZFMISC_1:33;
A89: yz' = z' + y' by A68, A70, ZFMISC_1:33;
then y'' <=' yz' by A75, ARYTM_2:20;
then not yz' <=' x' by A72, A69, A82, ARYTM_1:3;
hence + x,(+ y,z) = [0 ,((z' + y') -' x')] by A71, A89, ARYTM_1:def 2
.= [0 ,(z'' + (y'' -' x''))] by A72, A69, A75, A82, A88, ARYTM_1:13
.= + (+ x,y),z by A84, A85, A87, ZFMISC_1:33 ;
:: thesis:

end;

hence + x,(+ y,z) = + (+ x,y),z ; :: thesis:

end;

suppose that A90: z in REAL+ and
A91: y in REAL+ and
A92: x in [:{0 },REAL+ :] ; :: thesis:

A93: ex z'', y'' being Element of REAL+ st
( z = z'' & y = y'' & + z,y = z'' + y'' ) by A90, A91, Def2;
then consider zy'', x'' being Element of REAL+ such that
A94: + z,y = zy'' and
A95: x = [0 ,x''] and
A96: + (+ z,y),x = zy'' - x'' by A92, Def2;
consider y', x' being Element of REAL+ such that
A97: y = y' and
A98: x = [0 ,x'] and
A99: + y,x = y' - x' by A91, A92, Def2;
A100: x' = x'' by A98, A95, ZFMISC_1:33;

now

per cases ;

suppose A101: x' <=' y' ; :: thesis:

then A102: + y,x = y' -' x' by A99, ARYTM_1:def 2;
then ex z', yx' being Element of REAL+ st
( z = z' & + y,x = yx' & + z,(+ y,x) = z' + yx' ) by A90, Def2;
hence + z,(+ y,x) = + (+ z,y),x by A97, A93, A94, A96, A100, A101, A102, ARYTM_1:20; :: thesis:

end;

suppose A103: not x' <=' y' ; :: thesis:

then A104: + y,x = [0 ,(x' -' y')] by A99, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider z', yx' being Element of REAL+ such that
A105: z = z' and
A106: ( + y,x = [0 ,yx'] & + z,(+ y,x) = z' - yx' ) by A90, Def2;
thus + z,(+ y,x) = z' - (x' -' y') by A104, A106, ZFMISC_1:33
.= + (+ z,y),x by A97, A93, A94, A96, A100, A103, A105, ARYTM_1:21 ; :: thesis:

end;

hence + x,(+ y,z) = + (+ x,y),z ; :: thesis:

end;

suppose that A107: x in [:{0 },REAL+ :] and
A108: y in REAL+ and
A109: z in [:{0 },REAL+ :] ; :: thesis:

consider y', z' being Element of REAL+ such that
A110: y = y' and
A111: z = [0 ,z'] and
A112: + y,z = y' - z' by A108, A109, Def2;
consider x'', y'' being Element of REAL+ such that
A113: x = [0 ,x''] and
A114: y = y'' and
A115: + x,y = y'' - x'' by A107, A108, Def2;

now

per cases ;

suppose that A116: x'' <=' y'' and
A117: z' <=' y' ; :: thesis:

A118: + y,z = y' -' z' by A112, A117, ARYTM_1:def 2;
then consider x', yz' being Element of REAL+ such that
A119: x = [0 ,x'] and
A120: ( + y,z = yz' & + x,(+ y,z) = yz' - x' ) by A107, Def2;
A121: x' = x'' by A113, A119, ZFMISC_1:33;
then A122: + x,y = y' -' x' by A110, A114, A115, A116, ARYTM_1:def 2;
then consider z'', xy'' being Element of REAL+ such that
A123: z = [0 ,z''] and
A124: ( + x,y = xy'' & + z,(+ x,y) = xy'' - z'' ) by A109, Def2;
z' = z'' by A111, A123, ZFMISC_1:33;
hence + x,(+ y,z) = + (+ x,y),z by A110, A114, A116, A117, A118, A120, A121, A122, A124, ARYTM_1:25; :: thesis:

end;

suppose that A125: not x'' <=' y'' and
A126: z' <=' y' ; :: thesis:

A127: ( not z in REAL+ or not + x,y in [:{0 },REAL+ :] ) by A109, Th5, XBOOLE_0:3;
A128: + y,x = [0 ,(x'' -' y'')] by A115, A125, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( not + x,y in REAL+ or not z in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider z'', yx' being Element of REAL+ such that
A129: z = [0 ,z''] and
A130: ( + y,x = [0 ,yx'] & + z,(+ y,x) = [0 ,(z'' + yx')] ) by A128, A127, Def2, Lm1, ZFMISC_1:106;
A131: z' = z'' by A111, A129, ZFMISC_1:33;
A132: + y,z = y' -' z' by A112, A126, ARYTM_1:def 2;
then consider x', yz' being Element of REAL+ such that
A133: x = [0 ,x'] and
A134: + y,z = yz' and
A135: + x,(+ y,z) = yz' - x' by A107, Def2;
A136: x' = x'' by A113, A133, ZFMISC_1:33;
yz' <=' y' by A132, A134, ARYTM_1:11;
then not x' <=' yz' by A110, A114, A125, A136, ARYTM_1:3;
hence + x,(+ y,z) = [0 ,(x' -' (y' -' z'))] by A132, A134, A135, ARYTM_1:def 2
.= [0 ,((x'' -' y'') + z'')] by A110, A114, A125, A126, A136, A131, ARYTM_1:14
.= + (+ x,y),z by A128, A130, ZFMISC_1:33 ;
:: thesis:

end;

suppose that A137: not z' <=' y' and
A138: x'' <=' y'' ; :: thesis:

A139: ( not x in REAL+ or not + z,y in [:{0 },REAL+ :] ) by A107, Th5, XBOOLE_0:3;
A140: + y,z = [0 ,(z' -' y')] by A112, A137, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( not + z,y in REAL+ or not x in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider x', yz'' being Element of REAL+ such that
A141: x = [0 ,x'] and
A142: ( + y,z = [0 ,yz''] & + x,(+ y,z) = [0 ,(x' + yz'')] ) by A140, A139, Def2, Lm1, ZFMISC_1:106;
A143: x'' = x' by A113, A141, ZFMISC_1:33;
A144: + y,x = y'' -' x'' by A115, A138, ARYTM_1:def 2;
then consider z'', yx'' being Element of REAL+ such that
A145: z = [0 ,z''] and
A146: + y,x = yx'' and
A147: + z,(+ y,x) = yx'' - z'' by A109, Def2;
A148: z'' = z' by A111, A145, ZFMISC_1:33;
yx'' <=' y'' by A144, A146, ARYTM_1:11;
then A149: not z'' <=' yx'' by A110, A114, A137, A148, ARYTM_1:3;
thus + x,(+ y,z) = [0 ,((z' -' y') + x')] by A140, A142, ZFMISC_1:33
.= [0 ,(z'' -' (y'' -' x''))] by A110, A114, A137, A138, A148, A143, ARYTM_1:14
.= + (+ x,y),z by A144, A146, A147, A149, ARYTM_1:def 2 ; :: thesis:

end;

suppose that A150: not x'' <=' y'' and
A151: not z' <=' y' ; :: thesis:

A152: ( not x in REAL+ or not + z,y in [:{0 },REAL+ :] ) by A107, Th5, XBOOLE_0:3;
A153: ( not z in REAL+ or not + x,y in [:{0 },REAL+ :] ) by A109, Th5, XBOOLE_0:3;
A154: + y,x = [0 ,(x'' -' y'')] by A115, A150, ARYTM_1:def 2;
then + y,x in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( not + x,y in REAL+ or not z in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider z'', yx' being Element of REAL+ such that
A155: z = [0 ,z''] and
A156: ( + y,x = [0 ,yx'] & + z,(+ y,x) = [0 ,(z'' + yx')] ) by A154, A153, Def2, Lm1, ZFMISC_1:106;
A157: z' = z'' by A111, A155, ZFMISC_1:33;
A158: + y,z = [0 ,(z' -' y')] by A112, A151, ARYTM_1:def 2;
then + y,z in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( not + z,y in REAL+ or not x in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider x', yz'' being Element of REAL+ such that
A159: x = [0 ,x'] and
A160: ( + y,z = [0 ,yz''] & + x,(+ y,z) = [0 ,(x' + yz'')] ) by A158, A152, Def2, Lm1, ZFMISC_1:106;
A161: x' = x'' by A113, A159, ZFMISC_1:33;
thus + x,(+ y,z) = [0 ,((z' -' y') + x')] by A158, A160, ZFMISC_1:33
.= [0 ,((x'' -' y'') + z'')] by A110, A114, A150, A151, A157, A161, ARYTM_1:15
.= + (+ x,y),z by A154, A156, ZFMISC_1:33 ; :: thesis:

end;

hence + x,(+ y,z) = + (+ x,y),z ; :: thesis:

end;

suppose that A162: z in REAL+ and
A163: y in [:{0 },REAL+ :] and
A164: x in [:{0 },REAL+ :] ; :: thesis:

( ( not x in REAL+ or not y in [:{0 },REAL+ :] ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] ) ) by A163, A164, Th5, XBOOLE_0:3;
then consider y', x' being Element of REAL+ such that
A165: y = [0 ,y'] and
A166: x = [0 ,x'] and
A167: + y,x = [0 ,(y' + x')] by A163, Def2;
+ y,x in [:{0 },REAL+ :] by A167, Lm1, ZFMISC_1:106;
then consider z', yx' being Element of REAL+ such that
A168: z = z' and
A169: + y,x = [0 ,yx'] and
A170: + z,(+ y,x) = z' - yx' by A162, Def2;
consider z'', y'' being Element of REAL+ such that
A171: z = z'' and
A172: y = [0 ,y''] and
A173: + z,y = z'' - y'' by A162, A163, Def2;
A174: y' = y'' by A165, A172, ZFMISC_1:33;

now

per cases ;

suppose A175: y'' <=' z'' ; :: thesis:

then A176: + z,y = z'' -' y'' by A173, ARYTM_1:def 2;
then consider zy'', x'' being Element of REAL+ such that
A177: + z,y = zy'' and
A178: x = [0 ,x''] and
A179: + (+ z,y),x = zy'' - x'' by A164, Def2;
A180: x' = x'' by A166, A178, ZFMISC_1:33;
thus + z,(+ y,x) = z' - (y' + x') by A167, A169, A170, ZFMISC_1:33
.= + (+ z,y),x by A171, A168, A174, A175, A176, A177, A179, A180, ARYTM_1:24 ; :: thesis:

end;

suppose A181: not y'' <=' z'' ; :: thesis:

A182: ( not x in REAL+ or not + z,y in [:{0 },REAL+ :] ) by A164, Th5, XBOOLE_0:3;
A183: + z,y = [0 ,(y'' -' z'')] by A173, A181, ARYTM_1:def 2;
then + z,y in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then ( not + z,y in REAL+ or not x in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider zy'', x'' being Element of REAL+ such that
A184: + z,y = [0 ,zy''] and
A185: x = [0 ,x''] and
A186: + (+ z,y),x = [0 ,(zy'' + x'')] by A183, A182, Def2, Lm1, ZFMISC_1:106;
A187: x' = x'' by A166, A185, ZFMISC_1:33;
A188: yx' = x' + y' by A167, A169, ZFMISC_1:33;
then y'' <=' yx' by A174, ARYTM_2:20;
then not yx' <=' z' by A171, A168, A181, ARYTM_1:3;
hence + z,(+ y,x) = [0 ,((x' + y') -' z')] by A170, A188, ARYTM_1:def 2
.= [0 ,(x'' + (y'' -' z''))] by A171, A168, A174, A181, A187, ARYTM_1:13
.= + (+ z,y),x by A183, A184, A186, ZFMISC_1:33 ;
:: thesis:

end;

hence + x,(+ y,z) = + (+ x,y),z ; :: thesis:

end;

suppose that A189: x in [:{0 },REAL+ :] and
A190: y in [:{0 },REAL+ :] and
A191: z in [:{0 },REAL+ :] ; :: thesis:

A192: ( not x in REAL+ or not + z,y in [:{0 },REAL+ :] ) by A189, Th5, XBOOLE_0:3;
( ( not z in REAL+ or not y in [:{0 },REAL+ :] ) & ( not y in REAL+ or not z in [:{0 },REAL+ :] ) ) by A190, A191, Th5, XBOOLE_0:3;
then consider y', z' being Element of REAL+ such that
A193: y = [0 ,y'] and
A194: z = [0 ,z'] and
A195: + y,z = [0 ,(y' + z')] by A190, Def2;
+ z,y in [:{0 },REAL+ :] by A195, Lm1, ZFMISC_1:106;
then ( not + z,y in REAL+ or not x in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider x', yz' being Element of REAL+ such that
A196: x = [0 ,x'] and
A197: ( + y,z = [0 ,yz'] & + x,(+ y,z) = [0 ,(x' + yz')] ) by A195, A192, Def2, Lm1, ZFMISC_1:106;
A198: ( not z in REAL+ or not + x,y in [:{0 },REAL+ :] ) by A191, Th5, XBOOLE_0:3;
( ( not x in REAL+ or not y in [:{0 },REAL+ :] ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] ) ) by A189, A190, Th5, XBOOLE_0:3;
then consider x'', y'' being Element of REAL+ such that
A199: x = [0 ,x''] and
A200: y = [0 ,y''] and
A201: + x,y = [0 ,(x'' + y'')] by A189, Def2;
A202: x' = x'' by A199, A196, ZFMISC_1:33;
+ x,y in [:{0 },REAL+ :] by A201, Lm1, ZFMISC_1:106;
then ( not + x,y in REAL+ or not z in [:{0 },REAL+ :] ) by Th5, XBOOLE_0:3;
then consider xy'', z'' being Element of REAL+ such that
A203: + x,y = [0 ,xy''] and
A204: z = [0 ,z''] and
A205: + (+ x,y),z = [0 ,(xy'' + z'')] by A201, A198, Def2, Lm1, ZFMISC_1:106;
A206: z' = z'' by A194, A204, ZFMISC_1:33;
A207: y' = y'' by A193, A200, ZFMISC_1:33;
thus + x,(+ y,z) = [0 ,((z' + y') + x')] by A195, A197, ZFMISC_1:33
.= [0 ,(z'' + (y'' + x''))] by A206, A202, A207, ARYTM_2:7
.= + (+ x,y),z by A201, A203, A205, ZFMISC_1:33 ; :: thesis:

end;