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:

consider y', z' being Element of REAL+ such that
A4: y = y' and
A5: z = z' and
A6: * y,z = y' *' z' by A2, A3, Def3;
consider x', yz' being Element of REAL+ such that
A7: x = x' and
A8: * y,z = yz' and
A9: * x,(* y,z) = x' *' yz' by A1, A6, Def3;
consider x'', y'' being Element of REAL+ such that
A10: x = x'' and
A11: y = y'' and
A12: * x,y = x'' *' y'' by A1, A2, Def3;
consider xy'', z'' being Element of REAL+ such that
A13: * x,y = xy'' and
A14: z = z'' and
A15: * (* x,y),z = xy'' *' z'' by A3, A12, Def3;
thus * x,(* y,z) = * (* x,y),z by A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, ARYTM_2:13; :: thesis:

end;

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

consider y', z' being Element of REAL+ such that
A19: y = [0 ,y'] and
A20: z = z' and
A21: * y,z = [0 ,(z' *' y')] by A17, A18, Def3;
* y,z in [:{0 },REAL+ :] by A21, Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A22: x = x' and
A23: * y,z = [0 ,yz'] and
A24: * x,(* y,z) = [0 ,(x' *' yz')] by A16, Def3;
consider x'', y'' being Element of REAL+ such that
A25: x = x'' and
A26: y = [0 ,y''] and
A27: * x,y = [0 ,(x'' *' y'')] by A16, A17, Def3;
* x,y in [:{0 },REAL+ :] by A27, Lm1, ZFMISC_1:106;
then consider xy'', z'' being Element of REAL+ such that
A28: * x,y = [0 ,xy''] and
A29: z = z'' and
A30: * (* x,y),z = [0 ,(z'' *' xy'')] by A18, Def3;
A31: y' = y'' by A19, A26, ZFMISC_1:33;
thus * x,(* y,z) = [0 ,(x' *' (y' *' z'))] by A21, A23, A24, ZFMISC_1:33
.= [0 ,((x'' *' y'') *' z'')] by A20, A22, A25, A29, A31, ARYTM_2:13
.= * (* x,y),z by A27, A28, A30, ZFMISC_1:33 ; :: thesis:

end;

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

consider y', z' being Element of REAL+ such that
A35: y = y' and
A36: z = z' and
A37: * y,z = y' *' z' by A33, A34, Def3;
y' *' z' <> 0 by A33, A34, A35, A36, ARYTM_1:2;
then consider x', yz' being Element of REAL+ such that
A38: x = [0 ,x'] and
A39: * y,z = yz' and
A40: * x,(* y,z) = [0 ,(yz' *' x')] by A32, A37, Def3;
consider x'', y'' being Element of REAL+ such that
A41: x = [0 ,x''] and
A42: y = y'' and
A43: * x,y = [0 ,(y'' *' x'')] by A32, A33, Def3;
* x,y in [:{0 },REAL+ :] by A43, Lm1, ZFMISC_1:106;
then consider xy'', z'' being Element of REAL+ such that
A44: * x,y = [0 ,xy''] and
A45: z = z'' and
A46: * (* x,y),z = [0 ,(z'' *' xy'')] by A34, Def3;
x' = x'' by A38, A41, ZFMISC_1:33;
hence * x,(* y,z) = [0 ,((x'' *' y'') *' z'')] by A35, A36, A37, A39, A40, A42, A45, ARYTM_2:13
.= * (* x,y),z by A43, A44, A46, ZFMISC_1:33 ;
:: thesis:

end;

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

consider y', z' being Element of REAL+ such that
A50: y = [0 ,y'] and
A51: z = z' and
A52: * y,z = [0 ,(z' *' y')] by A48, A49, Def3;
* y,z in [:{0 },REAL+ :] by A52, Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A53: x = [0 ,x'] and
A54: * y,z = [0 ,yz'] and
A55: * x,(* y,z) = yz' *' x' by A47, Def3;
consider x'', y'' being Element of REAL+ such that
A56: x = [0 ,x''] and
A57: y = [0 ,y''] and
A58: * x,y = y'' *' x'' by A47, A48, Def3;
consider xy'', z'' being Element of REAL+ such that
A59: * x,y = xy'' and
A60: z = z'' and
A61: * (* x,y),z = xy'' *' z'' by A49, A58, Def3;
A62: x' = x'' by A53, A56, ZFMISC_1:33;
A63: y' = y'' by A50, A57, ZFMISC_1:33;
thus * x,(* y,z) = x' *' (y' *' z') by A52, A54, A55, ZFMISC_1:33
.= * (* x,y),z by A51, A58, A59, A60, A61, A62, A63, ARYTM_2:13 ; :: thesis:

end;

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

consider y', z' being Element of REAL+ such that
A67: y = y' and
A68: z = [0 ,z'] and
A69: * y,z = [0 ,(y' *' z')] by A65, A66, Def3;
* y,z in [:{0 },REAL+ :] by A69, Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A70: x = x' and
A71: * y,z = [0 ,yz'] and
A72: * x,(* y,z) = [0 ,(x' *' yz')] by A64, Def3;
consider x'', y'' being Element of REAL+ such that
A73: x = x'' and
A74: y = y'' and
A75: * x,y = x'' *' y'' by A64, A65, Def3;
* x,y <> 0 by A64, A65, A73, A74, A75, ARYTM_1:2;
then consider xy'', z'' being Element of REAL+ such that
A76: * x,y = xy'' and
A77: z = [0 ,z''] and
A78: * (* x,y),z = [0 ,(xy'' *' z'')] by A66, A75, Def3;
A79: z' = z'' by A68, A77, ZFMISC_1:33;
thus * x,(* y,z) = [0 ,(x' *' (y' *' z'))] by A69, A71, A72, ZFMISC_1:33
.= * (* x,y),z by A67, A70, A73, A74, A75, A76, A78, A79, ARYTM_2:13 ; :: thesis:

end;

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

consider y', z' being Element of REAL+ such that
A83: y = [0 ,y'] and
A84: z = [0 ,z'] and
A85: * y,z = z' *' y' by A81, A82, Def3;
consider x', yz' being Element of REAL+ such that
A86: x = x' and
A87: * y,z = yz' and
A88: * x,(* y,z) = x' *' yz' by A80, A85, Def3;
consider x'', y'' being Element of REAL+ such that
A89: x = x'' and
A90: y = [0 ,y''] and
A91: * x,y = [0 ,(x'' *' y'')] by A80, A81, Def3;
* x,y in [:{0 },REAL+ :] by A91, Lm1, ZFMISC_1:106;
then consider xy'', z'' being Element of REAL+ such that
A92: * x,y = [0 ,xy''] and
A93: z = [0 ,z''] and
A94: * (* x,y),z = z'' *' xy'' by A82, Def3;
A95: y' = y'' by A83, A90, ZFMISC_1:33;
z' = z'' by A84, A93, ZFMISC_1:33;
hence * x,(* y,z) = (x'' *' y'') *' z'' by A85, A86, A87, A88, A89, A95, ARYTM_2:13
.= * (* x,y),z by A91, A92, A94, ZFMISC_1:33 ;
:: thesis:

end;

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

consider y', z' being Element of REAL+ such that
A99: y = y' and
A100: z = [0 ,z'] and
A101: * y,z = [0 ,(y' *' z')] by A96, A98, Def3;
[0 ,(y' *' z')] in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A102: x = [0 ,x'] and
A103: * y,z = [0 ,yz'] and
A104: * x,(* y,z) = yz' *' x' by A97, A101, Def3;
consider x'', y'' being Element of REAL+ such that
A105: x = [0 ,x''] and
A106: y = y'' and
A107: * x,y = [0 ,(y'' *' x'')] by A96, A97, Def3;
* x,y in [:{0 },REAL+ :] by A107, Lm1, ZFMISC_1:106;
then consider xy'', z'' being Element of REAL+ such that
A108: * x,y = [0 ,xy''] and
A109: z = [0 ,z''] and
A110: * (* x,y),z = z'' *' xy'' by A98, Def3;
A111: x' = x'' by A102, A105, ZFMISC_1:33;
A112: z' = z'' by A100, A109, ZFMISC_1:33;
thus * x,(* y,z) = x' *' (y' *' z') by A101, A103, A104, ZFMISC_1:33
.= (x'' *' y'') *' z'' by A99, A106, A111, A112, ARYTM_2:13
.= * (* x,y),z by A107, A108, A110, ZFMISC_1:33 ; :: thesis:

end;

suppose that A113: x in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A114: y in [:{0 },REAL+ :] \ {[0 ,0 ]} and
A115: z in [:{0 },REAL+ :] \ {[0 ,0 ]} ; :: thesis:

consider y', z' being Element of REAL+ such that
A116: y = [0 ,y'] and
A117: z = [0 ,z'] and
A118: * y,z = z' *' y' by A114, A115, Def3;
( not z in {[0 ,0 ]} & not y in {[0 ,0 ]} ) by A114, A115, XBOOLE_0:def 5;
then ( z' <> 0 & y' <> 0 ) by A116, A117, TARSKI:def 1;
then * z,y <> 0 by A118, ARYTM_1:2;
then consider x', yz' being Element of REAL+ such that
A119: x = [0 ,x'] and
A120: * y,z = yz' and
A121: * x,(* y,z) = [0 ,(yz' *' x')] by A113, A118, Def3;
consider x'', y'' being Element of REAL+ such that
A122: x = [0 ,x''] and
A123: y = [0 ,y''] and
A124: * x,y = y'' *' x'' by A113, A114, Def3;
A125: x' = x'' by A119, A122, ZFMISC_1:33;
A126: y' = y'' by A116, A123, ZFMISC_1:33;
( not x in {[0 ,0 ]} & not y in {[0 ,0 ]} ) by A113, A114, XBOOLE_0:def 5;
then ( x' <> 0 & y' <> 0 ) by A116, A119, TARSKI:def 1;
then * x,y <> 0 by A124, A125, A126, ARYTM_1:2;
then consider xy'', z'' being Element of REAL+ such that
A127: * x,y = xy'' and
A128: z = [0 ,z''] and
A129: * (* x,y),z = [0 ,(xy'' *' z'')] by A115, A124, Def3;
z' = z'' by A117, A128, ZFMISC_1:33;
hence * x,(* y,z) = * (* x,y),z by A118, A120, A121, A124, A125, A126, A127, A129, ARYTM_2:13; :: thesis:

end;

suppose A130: x = 0 ; :: thesis:

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

end;

suppose A131: y = 0 ; :: thesis:

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

end;

suppose A132: z = 0 ; :: thesis:

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

end;

suppose A133: ( ( 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:

A134: 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 A134, ZFMISC_1:65 ;
hence * x,(* y,z) = * (* x,y),z by A133, XBOOLE_0:def 3; :: thesis:

end;