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 x'', y'' being Element of REAL+ st
( x = x'' & y = y'' & * x,y = x'' *' y'' ) by A1, A2, Def3;
then A5: ex xy'', z'' being Element of REAL+ st
( * x,y = xy'' & z = z'' & * (* x,y),z = xy'' *' z'' ) by A3, Def3;
A6: ex y', z' being Element of REAL+ st
( y = y' & z = z' & * y,z = y' *' z' ) by A2, A3, Def3;
then ex x', yz' being Element of REAL+ st
( x = x' & * y,z = yz' & * x,(* y,z) = x' *' yz' ) 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 y', z' being Element of REAL+ such that
A10: y = [0 ,y'] and
A11: z = z' and
A12: * y,z = [0 ,(z' *' y')] by A8, A9, Def3;
* y,z in [:{0 },REAL+ :] by A12, Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A13: x = x' and
A14: ( * y,z = [0 ,yz'] & * x,(* y,z) = [0 ,(x' *' yz')] ) by A7, Def3;
consider x'', y'' being Element of REAL+ such that
A15: x = x'' and
A16: y = [0 ,y''] and
A17: * x,y = [0 ,(x'' *' y'')] by A7, A8, Def3;
A18: y' = y'' by A10, A16, ZFMISC_1:33;
* x,y in [:{0 },REAL+ :] by A17, Lm1, ZFMISC_1:106;
then consider xy'', z'' being Element of REAL+ such that
A19: * x,y = [0 ,xy''] and
A20: z = z'' and
A21: * (* x,y),z = [0 ,(z'' *' xy'')] by A9, Def3;
thus * x,(* y,z) = [0 ,(x' *' (y' *' z'))] by A12, A14, ZFMISC_1:33
.= [0 ,((x'' *' y'') *' z'')] 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 y', z' being Element of REAL+ such that
A25: ( y = y' & z = z' ) and
A26: * y,z = y' *' z' by A23, A24, Def3;
y' *' z' <> 0 by A23, A24, A25, ARYTM_1:2;
then consider x', yz' being Element of REAL+ such that
A27: x = [0 ,x'] and
A28: ( * y,z = yz' & * x,(* y,z) = [0 ,(yz' *' x')] ) by A22, A26, Def3;
consider x'', y'' being Element of REAL+ such that
A29: x = [0 ,x''] and
A30: y = y'' and
A31: * x,y = [0 ,(y'' *' x'')] by A22, A23, Def3;
* x,y in [:{0 },REAL+ :] by A31, Lm1, ZFMISC_1:106;
then consider xy'', z'' being Element of REAL+ such that
A32: * x,y = [0 ,xy''] and
A33: z = z'' and
A34: * (* x,y),z = [0 ,(z'' *' xy'')] by A24, Def3;
x' = x'' by A27, A29, ZFMISC_1:33;
hence * x,(* y,z) = [0 ,((x'' *' y'') *' z'')] 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 x'', y'' being Element of REAL+ such that
A38: x = [0 ,x''] and
A39: y = [0 ,y''] and
A40: * x,y = y'' *' x'' by A35, A36, Def3;
consider y', z' being Element of REAL+ such that
A41: y = [0 ,y'] and
A42: z = z' and
A43: * y,z = [0 ,(z' *' y')] by A36, A37, Def3;
A44: y' = y'' by A41, A39, ZFMISC_1:33;
* y,z in [:{0 },REAL+ :] by A43, Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A45: x = [0 ,x'] and
A46: ( * y,z = [0 ,yz'] & * x,(* y,z) = yz' *' x' ) by A35, Def3;
A47: x' = x'' by A45, A38, ZFMISC_1:33;
A48: ex xy'', z'' being Element of REAL+ st
( * x,y = xy'' & z = z'' & * (* x,y),z = xy'' *' z'' ) by A37, A40, Def3;
thus * x,(* y,z) = x' *' (y' *' z') 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 x'', y'' being Element of REAL+ st
( x = x'' & y = y'' & * x,y = x'' *' y'' ) by A49, A50, Def3;
then * x,y <> 0 by A49, A50, ARYTM_1:2;
then consider xy'', z'' being Element of REAL+ such that
A53: * x,y = xy'' and
A54: z = [0 ,z''] and
A55: * (* x,y),z = [0 ,(xy'' *' z'')] by A51, A52, Def3;
consider y', z' being Element of REAL+ such that
A56: y = y' and
A57: z = [0 ,z'] and
A58: * y,z = [0 ,(y' *' z')] by A50, A51, Def3;
A59: z' = z'' by A57, A54, ZFMISC_1:33;
* y,z in [:{0 },REAL+ :] by A58, Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A60: x = x' and
A61: ( * y,z = [0 ,yz'] & * x,(* y,z) = [0 ,(x' *' yz')] ) by A49, Def3;
thus * x,(* y,z) = [0 ,(x' *' (y' *' z'))] 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 y', z' being Element of REAL+ such that
A65: y = [0 ,y'] and
A66: z = [0 ,z'] and
A67: * y,z = z' *' y' by A63, A64, Def3;
A68: ex x', yz' being Element of REAL+ st
( x = x' & * y,z = yz' & * x,(* y,z) = x' *' yz' ) by A62, A67, Def3;
consider x'', y'' being Element of REAL+ such that
A69: x = x'' and
A70: y = [0 ,y''] and
A71: * x,y = [0 ,(x'' *' y'')] by A62, A63, Def3;
A72: y' = y'' by A65, A70, ZFMISC_1:33;
* x,y in [:{0 },REAL+ :] by A71, Lm1, ZFMISC_1:106;
then consider xy'', z'' being Element of REAL+ such that
A73: * x,y = [0 ,xy''] and
A74: z = [0 ,z''] and
A75: * (* x,y),z = z'' *' xy'' by A64, Def3;
z' = z'' by A66, A74, ZFMISC_1:33;
hence * x,(* y,z) = (x'' *' y'') *' z'' 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 x'', y'' being Element of REAL+ such that
A79: x = [0 ,x''] and
A80: y = y'' and
A81: * x,y = [0 ,(y'' *' x'')] by A76, A77, Def3;
consider y', z' being Element of REAL+ such that
A82: y = y' and
A83: z = [0 ,z'] and
A84: * y,z = [0 ,(y' *' z')] by A76, A78, Def3;
[0 ,(y' *' z')] in [:{0 },REAL+ :] by Lm1, ZFMISC_1:106;
then consider x', yz' being Element of REAL+ such that
A85: x = [0 ,x'] and
A86: ( * y,z = [0 ,yz'] & * x,(* y,z) = yz' *' x' ) by A77, A84, Def3;
A87: x' = x'' by A85, A79, ZFMISC_1:33;
* x,y in [:{0 },REAL+ :] by A81, Lm1, ZFMISC_1:106;
then consider xy'', z'' being Element of REAL+ such that
A88: * x,y = [0 ,xy''] and
A89: z = [0 ,z''] and
A90: * (* x,y),z = z'' *' xy'' by A78, Def3;
A91: z' = z'' by A83, A89, ZFMISC_1:33;
thus * x,(* y,z) = x' *' (y' *' z') by A84, A86, ZFMISC_1:33
.= (x'' *' y'') *' z'' 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 y', z' being Element of REAL+ such that
A95: y = [0 ,y'] and
A96: z = [0 ,z'] and
A97: * y,z = z' *' y' by A93, A94, Def3;
not y in {[0 ,0 ]} by A93, XBOOLE_0:def 5;
then A98: y' <> 0 by A95, TARSKI:def 1;
not z in {[0 ,0 ]} by A94, XBOOLE_0:def 5;
then z' <> 0 by A96, TARSKI:def 1;
then * z,y <> 0 by A97, A98, ARYTM_1:2;
then consider x', yz' being Element of REAL+ such that
A99: x = [0 ,x'] and
A100: ( * y,z = yz' & * x,(* y,z) = [0 ,(yz' *' x')] ) by A92, A97, Def3;
consider x'', y'' being Element of REAL+ such that
A101: x = [0 ,x''] and
A102: y = [0 ,y''] and
A103: * x,y = y'' *' x'' by A92, A93, Def3;
A104: x' = x'' by A99, A101, ZFMISC_1:33;
A105: y' = y'' by A95, A102, ZFMISC_1:33;
not y in {[0 ,0 ]} by A93, XBOOLE_0:def 5;
then A106: y' <> 0 by A95, TARSKI:def 1;
not x in {[0 ,0 ]} by A92, XBOOLE_0:def 5;
then x' <> 0 by A99, TARSKI:def 1;
then * x,y <> 0 by A103, A104, A105, A106, ARYTM_1:2;
then consider xy'', z'' being Element of REAL+ such that
A107: * x,y = xy'' and
A108: z = [0 ,z''] and
A109: * (* x,y),z = [0 ,(xy'' *' z'')] by A94, A103, Def3;
z' = z'' 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;