let x, y, z be Element of REAL ; :: thesis:

suppose that A1: x in REAL+ and
A2: y in REAL+ and
A3: z in REAL+ ; :: thesis:

A4: ex x99, y99 being Element of REAL+ st
( x = x99 & y = y99 & * x,y = x99 *' y99 ) by A1, A2, Def3;
then A5: ex xy99, z99 being Element of REAL+ st
( * x,y = xy99 & z = z99 & * (* x,y),z = xy99 *' z99 ) by A3, Def3;
A6: ex y9, z9 being Element of REAL+ st
( y = y9 & z = z9 & * y,z = y9 *' z9 ) by A2, A3, Def3;
then ex x9, yz9 being Element of REAL+ st
( x = x9 & * y,z = yz9 & * x,(* y,z) = x9 *' yz9 ) by A1, Def3;
hence * x,(* y,z) = * (* x,y),z by A6, A4, A5, ARYTM_2:13; :: thesis:

end;

suppose that A7: ( x in REAL+ & x <> 0 ) and
A8: y in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A9: ( z in REAL+ & z <> 0 ) ; :: thesis:

consider y9, z9 being Element of REAL+ such that
A10: y = [0 ,y9] and
A11: z = z9 and
A12: * y,z = [0 ,(z9 *' y9)] by A8, A9, Def3;
* y,z in [:{0 },REAL+ :] by A12, Lm1, ZFMISC_1:106;
then consider x9, yz9 being Element of REAL+ such that
A13: x = x9 and
A14: ( * y,z = [0 ,yz9] & * x,(* y,z) = [0 ,(x9 *' yz9)] ) by A7, Def3;
consider x99, y99 being Element of REAL+ such that
A15: x = x99 and
A16: y = [0 ,y99] and
A17: * x,y = [0 ,(x99 *' y99)] by A7, A8, Def3;
A18: y9 = y99 by A10, A16, ZFMISC_1:33;
* x,y in [:{0 },REAL+ :] by A17, Lm1, ZFMISC_1:106;
then consider xy99, z99 being Element of REAL+ such that
A19: * x,y = [0 ,xy99] and
A20: z = z99 and
A21: * (* x,y),z = [0 ,(z99 *' xy99)] by A9, Def3;
thus * x,(* y,z) = [0 ,(x9 *' (y9 *' z9))] by A12, A14, ZFMISC_1:33
.= [0 ,((x99 *' y99) *' z99)] by A11, A13, A15, A20, A18, ARYTM_2:13
.= * (* x,y),z by A17, A19, A21, ZFMISC_1:33 ; :: thesis:

end;

suppose that A22: x in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A23: ( y in REAL+ & y <> 0 ) and
A24: ( z in REAL+ & z <> 0 ) ; :: thesis:

consider y9, z9 being Element of REAL+ such that
A25: ( y = y9 & z = z9 ) and
A26: * y,z = y9 *' z9 by A23, A24, Def3;
y9 *' z9 <> 0 by A23, A24, A25, ARYTM_1:2;
then consider x9, yz9 being Element of REAL+ such that
A27: x = [0 ,x9] and
A28: ( * y,z = yz9 & * x,(* y,z) = [0 ,(yz9 *' x9)] ) by A22, A26, Def3;
consider x99, y99 being Element of REAL+ such that
A29: x = [0 ,x99] and
A30: y = y99 and
A31: * x,y = [0 ,(y99 *' x99)] by A22, A23, Def3;
* x,y in [:{0 },REAL+ :] by A31, Lm1, ZFMISC_1:106;
then consider xy99, z99 being Element of REAL+ such that
A32: * x,y = [0 ,xy99] and
A33: z = z99 and
A34: * (* x,y),z = [0 ,(z99 *' xy99)] by A24, Def3;
x9 = x99 by A27, A29, ZFMISC_1:33;
hence * x,(* y,z) = [0 ,((x99 *' y99) *' z99)] by A25, A26, A28, A30, A33, ARYTM_2:13
.= * (* x,y),z by A31, A32, A34, ZFMISC_1:33 ;
:: thesis:

end;

suppose that A35: x in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A36: y in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A37: ( z in REAL+ & z <> 0 ) ; :: thesis:

consider x99, y99 being Element of REAL+ such that
A38: x = [0 ,x99] and
A39: y = [0 ,y99] and
A40: * x,y = y99 *' x99 by A35, A36, Def3;
consider y9, z9 being Element of REAL+ such that
A41: y = [0 ,y9] and
A42: z = z9 and
A43: * y,z = [0 ,(z9 *' y9)] by A36, A37, Def3;
A44: y9 = y99 by A41, A39, ZFMISC_1:33;
* y,z in [:{0 },REAL+ :] by A43, Lm1, ZFMISC_1:106;
then consider x9, yz9 being Element of REAL+ such that
A45: x = [0 ,x9] and
A46: ( * y,z = [0 ,yz9] & * x,(* y,z) = yz9 *' x9 ) by A35, Def3;
A47: x9 = x99 by A45, A38, ZFMISC_1:33;
A48: ex xy99, z99 being Element of REAL+ st
( * x,y = xy99 & z = z99 & * (* x,y),z = xy99 *' z99 ) by A37, A40, Def3;
thus * x,(* y,z) = x9 *' (y9 *' z9) by A43, A46, ZFMISC_1:33
.= * (* x,y),z by A42, A40, A48, A47, A44, ARYTM_2:13 ; :: thesis:

end;

suppose that A49: ( x in REAL+ & x <> 0 ) and
A50: ( y in REAL+ & y <> 0 ) and
A51: z in [:{0 },REAL+ :] \ {[0 ,0 ]} ; :: thesis:

A52: ex x99, y99 being Element of REAL+ st
( x = x99 & y = y99 & * x,y = x99 *' y99 ) by A49, A50, Def3;
then * x,y <> 0 by A49, A50, ARYTM_1:2;
then consider xy99, z99 being Element of REAL+ such that
A53: * x,y = xy99 and
A54: z = [0 ,z99] and
A55: * (* x,y),z = [0 ,(xy99 *' z99)] by A51, A52, Def3;
consider y9, z9 being Element of REAL+ such that
A56: y = y9 and
A57: z = [0 ,z9] and
A58: * y,z = [0 ,(y9 *' z9)] by A50, A51, Def3;
A59: z9 = z99 by A57, A54, ZFMISC_1:33;
* y,z in [:{0 },REAL+ :] by A58, Lm1, ZFMISC_1:106;
then consider x9, yz9 being Element of REAL+ such that
A60: x = x9 and
A61: ( * y,z = [0 ,yz9] & * x,(* y,z) = [0 ,(x9 *' yz9)] ) by A49, Def3;
thus * x,(* y,z) = [0 ,(x9 *' (y9 *' z9))] by A58, A61, ZFMISC_1:33
.= * (* x,y),z by A56, A60, A52, A53, A55, A59, ARYTM_2:13 ; :: thesis:

end;

suppose that A62: ( x in REAL+ & x <> 0 ) and
A63: y in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A64: z in [:{0 },REAL+ :] \ {[0 ,0 ]} ; :: thesis:

consider y9, z9 being Element of REAL+ such that
A65: y = [0 ,y9] and
A66: z = [0 ,z9] and
A67: * y,z = z9 *' y9 by A63, A64, Def3;
A68: ex x9, yz9 being Element of REAL+ st
( x = x9 & * y,z = yz9 & * x,(* y,z) = x9 *' yz9 ) by A62, A67, Def3;
consider x99, y99 being Element of REAL+ such that
A69: x = x99 and
A70: y = [0 ,y99] and
A71: * x,y = [0 ,(x99 *' y99)] by A62, A63, Def3;
A72: y9 = y99 by A65, A70, ZFMISC_1:33;
* x,y in [:{0 },REAL+ :] by A71, Lm1, ZFMISC_1:106;
then consider xy99, z99 being Element of REAL+ such that
A73: * x,y = [0 ,xy99] and
A74: z = [0 ,z99] and
A75: * (* x,y),z = z99 *' xy99 by A64, Def3;
z9 = z99 by A66, A74, ZFMISC_1:33;
hence * x,(* y,z) = (x99 *' y99) *' z99 by A67, A68, A69, A72, ARYTM_2:13
.= * (* x,y),z by A71, A73, A75, ZFMISC_1:33 ;
:: thesis:

end;

suppose that A76: ( y in REAL+ & y <> 0 ) and
A77: x in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A78: z in [:{0 },REAL+ :] \ {[0 ,0 ]} ; :: thesis:

consider x99, y99 being Element of REAL+ such that
A79: x = [0 ,x99] and
A80: y = y99 and
A81: * x,y = [0 ,(y99 *' x99)] by A76, A77, Def3;
consider y9, z9 being Element of REAL+ such that
A82: y = y9 and
A83: z = [0 ,z9] and
A84: * y,z = [0 ,(y9 *' z9)] by A76, A78, Def3;
[0 ,(y9 *' z9)] in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider x9, yz9 being Element of REAL+ such that
A85: x = [0 ,x9] and
A86: ( * y,z = [0 ,yz9] & * x,(* y,z) = yz9 *' x9 ) by A77, A84, Def3;
A87: x9 = x99 by A85, A79, ZFMISC_1:33;
* x,y in [:{0 },REAL+ :] by A81, Lm1, ZFMISC_1:106;
then consider xy99, z99 being Element of REAL+ such that
A88: * x,y = [0 ,xy99] and
A89: z = [0 ,z99] and
A90: * (* x,y),z = z99 *' xy99 by A78, Def3;
A91: z9 = z99 by A83, A89, ZFMISC_1:33;
thus * x,(* y,z) = x9 *' (y9 *' z9) by A84, A86, ZFMISC_1:33
.= (x99 *' y99) *' z99 by A82, A80, A87, A91, ARYTM_2:13
.= * (* x,y),z by A81, A88, A90, ZFMISC_1:33 ; :: thesis:

end;

suppose that A92: x in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A93: y in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A94: z in [:{0 },REAL+ :] \ {[0 ,0 ]} ; :: thesis:

consider y9, z9 being Element of REAL+ such that
A95: y = [0 ,y9] and
A96: z = [0 ,z9] and
A97: * y,z = z9 *' y9 by A93, A94, Def3;
not y in {[0 ,0 ]} by A93, XBOOLE_0:def 5;
then A98: y9 <> 0 by A95, TARSKI:def 1;
not z in {[0 ,0 ]} by A94, XBOOLE_0:def 5;
then z9 <> 0 by A96, TARSKI:def 1;
then * z,y <> 0 by A97, A98, ARYTM_1:2;
then consider x9, yz9 being Element of REAL+ such that
A99: x = [0 ,x9] and
A100: ( * y,z = yz9 & * x,(* y,z) = [0 ,(yz9 *' x9)] ) by A92, A97, Def3;
consider x99, y99 being Element of REAL+ such that
A101: x = [0 ,x99] and
A102: y = [0 ,y99] and
A103: * x,y = y99 *' x99 by A92, A93, Def3;
A104: x9 = x99 by A99, A101, ZFMISC_1:33;
A105: y9 = y99 by A95, A102, ZFMISC_1:33;
not y in {[0 ,0 ]} by A93, XBOOLE_0:def 5;
then A106: y9 <> 0 by A95, TARSKI:def 1;
not x in {[0 ,0 ]} by A92, XBOOLE_0:def 5;
then x9 <> 0 by A99, TARSKI:def 1;
then * x,y <> 0 by A103, A104, A105, A106, ARYTM_1:2;
then consider xy99, z99 being Element of REAL+ such that
A107: * x,y = xy99 and
A108: z = [0 ,z99] and
A109: * (* x,y),z = [0 ,(xy99 *' z99)] by A94, A103, Def3;
z9 = z99 by A96, A108, ZFMISC_1:33;
hence * x,(* y,z) = * (* x,y),z by A97, A100, A103, A104, A105, A107, A109, ARYTM_2:13; :: thesis:

end;

suppose A110: x = 0 ; :: thesis:

hence * x,(* y,z) = 0 by Th14
.= * o,z by Th14
.= * (* x,y),z by A110, Th14 ;
:: thesis:

end;

suppose A111: y = 0 ; :: thesis:

hence * x,(* y,z) = * x,o by Th14
.= 0 by Th14
.= * o,z by Th14
.= * (* x,y),z by A111, Th14 ;
:: thesis:

end;

suppose A112: z = 0 ; :: thesis:

hence * x,(* y,z) = * x,o by Th14
.= 0 by Th14
.= * (* x,y),z by A112, Th14 ;
:: thesis:

end;

suppose A113: ( ( not x in REAL+ or not y in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not z in REAL+ ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not z in REAL+ ) & ( not x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not z in REAL+ ) & ( not x in REAL+ or not y in REAL+ or not z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) & ( not x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) ) ; :: thesis:

A114: not [0 ,0 ] in REAL+ by ARYTM_2:3;
REAL = (REAL+ \ {[{} ,{} ]}) \/ ([:{{} },REAL+ :] \ {[{} ,{} ]}) by NUMBERS:def 1, XBOOLE_1:42
.= REAL+ \/ ([:{0 },REAL+ :] \ {[0 ,0 ]}) by A114, ZFMISC_1:65 ;
hence * x,(* y,z) = * (* x,y),z by A113, XBOOLE_0:def 3; :: thesis:

end;