let x, y, z be Element of REAL ; :: thesis:
reconsider o = 0 as Element of REAL by Lm3;

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, Def2;
then A5: ex xy99, z99 being Element of REAL+ st
( * (x,y) = xy99 & z = z99 & * ((* (x,y)),z) = xy99 *' z99 ) by A3, Def2;
A6: ex y9, z9 being Element of REAL+ st
( y = y9 & z = z9 & * (y,z) = y9 *' z9 ) by A2, A3, Def2;
then ex x9, yz9 being Element of REAL+ st
( x = x9 & * (y,z) = yz9 & * (x,(* (y,z))) = x9 *' yz9 ) by A1, Def2;
hence * (x,(* (y,z))) = * ((* (x,y)),z) by A6, A4, A5, ARYTM_2:12; :: 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, Def2;
* (y,z) in [:{0},REAL+:] by A12, Lm1;
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, Def2;
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, Def2;
A18: y9 = y99 by A10, A16, XTUPLE_0:1;
* (x,y) in [:{0},REAL+:] by A17, Lm1;
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, Def2;
thus * (x,(* (y,z))) = [0,(x9 *' (y9 *' z9))] by A12, A14, XTUPLE_0:1
.= [0,((x99 *' y99) *' z99)] by A11, A13, A15, A20, A18, ARYTM_2:12
.= * ((* (x,y)),z) by A17, A19, A21, XTUPLE_0:1 ; :: 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, Def2;
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, Def2;
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, Def2;
* (x,y) in [:{0},REAL+:] by A31, Lm1;
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, Def2;
x9 = x99 by A27, A29, XTUPLE_0:1;
hence * (x,(* (y,z))) = [0,((x99 *' y99) *' z99)] by A25, A26, A28, A30, A33, ARYTM_2:12
.= * ((* (x,y)),z) by A31, A32, A34, XTUPLE_0:1 ;
:: 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, Def2;
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, Def2;
A44: y9 = y99 by A41, A39, XTUPLE_0:1;
* (y,z) in [:{0},REAL+:] by A43, Lm1;
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, Def2;
A47: x9 = x99 by A45, A38, XTUPLE_0:1;
A48: ex xy99, z99 being Element of REAL+ st
( * (x,y) = xy99 & z = z99 & * ((* (x,y)),z) = xy99 *' z99 ) by A37, A40, Def2;
thus * (x,(* (y,z))) = x9 *' (y9 *' z9) by A43, A46, XTUPLE_0:1
.= * ((* (x,y)),z) by A42, A40, A48, A47, A44, ARYTM_2:12 ; :: 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, Def2;
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, Def2;
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, Def2;
A59: z9 = z99 by A57, A54, XTUPLE_0:1;
* (y,z) in [:{0},REAL+:] by A58, Lm1;
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, Def2;
thus * (x,(* (y,z))) = [0,(x9 *' (y9 *' z9))] by A58, A61, XTUPLE_0:1
.= * ((* (x,y)),z) by A56, A60, A52, A53, A55, A59, ARYTM_2:12 ; :: 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, Def2;
A68: ex x9, yz9 being Element of REAL+ st
( x = x9 & * (y,z) = yz9 & * (x,(* (y,z))) = x9 *' yz9 ) by A62, A67, Def2;
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, Def2;
A72: y9 = y99 by A65, A70, XTUPLE_0:1;
* (x,y) in [:{0},REAL+:] by A71, Lm1;
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, Def2;
z9 = z99 by A66, A74, XTUPLE_0:1;
hence * (x,(* (y,z))) = (x99 *' y99) *' z99 by A67, A68, A69, A72, ARYTM_2:12
.= * ((* (x,y)),z) by A71, A73, A75, XTUPLE_0:1 ;
:: 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, Def2;
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, Def2;
[0,(y9 *' z9)] in [:{0},REAL+:] by Lm1;
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, Def2;
A87: x9 = x99 by A85, A79, XTUPLE_0:1;
* (x,y) in [:{0},REAL+:] by A81, Lm1;
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, Def2;
A91: z9 = z99 by A83, A89, XTUPLE_0:1;
thus * (x,(* (y,z))) = x9 *' (y9 *' z9) by A84, A86, XTUPLE_0:1
.= (x99 *' y99) *' z99 by A82, A80, A87, A91, ARYTM_2:12
.= * ((* (x,y)),z) by A81, A88, A90, XTUPLE_0:1 ; :: 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, Def2;
not y in {[0,0]} by XBOOLE_0:def 5;
then A98: y9 <> 0 by A95, TARSKI:def 1;
not z in {[0,0]} by 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, Def2;
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, Def2;
A104: x9 = x99 by A99, A101, XTUPLE_0:1;
A105: y9 = y99 by A95, A102, XTUPLE_0:1;
not y in {[0,0]} by XBOOLE_0:def 5;
then A106: y9 <> 0 by A95, TARSKI:def 1;
not x in {[0,0]} by 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, Def2;
z9 = z99 by A96, A108, XTUPLE_0:1;
hence * (x,(* (y,z))) = * ((* (x,y)),z) by A97, A100, A103, A104, A105, A107, A109, ARYTM_2:12; :: thesis:

end;

suppose A110: x = 0 ; :: thesis:

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

end;

suppose A111: y = 0 ; :: thesis:

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

end;

suppose A112: z = 0 ; :: thesis:

hence * (x,(* (y,z))) = * (x,o) by Th12
.= 0 by Th12
.= * ((* (x,y)),z) by A112, Th12 ;
:: 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:

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

end;