let x, y, z be Element of REAL ; * (x,(* (y,z))) = * ((* (x,y)),z)
reconsider o = 0 as Element of REAL by Lm3;
per cases
( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & x <> 0 & y in [:{0},REAL+:] \ {[0,0]} & z in REAL+ & z <> 0 ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in REAL+ & y <> 0 & z in REAL+ & z <> 0 ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in [:{0},REAL+:] \ {[0,0]} & z in REAL+ & z <> 0 ) or ( x in REAL+ & x <> 0 & y in REAL+ & y <> 0 & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in REAL+ & x <> 0 & y in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or ( y in REAL+ & y <> 0 & x in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or x = 0 or y = 0 or z = 0 or ( ( 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]} ) ) )
;
suppose that A1:
x in REAL+
and A2:
y in REAL+
and A3:
z in REAL+
;
* (x,(* (y,z))) = * ((* (x,y)),z)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;
verum end; suppose that A7:
(
x in REAL+ &
x <> 0 )
and A8:
y in [:{0},REAL+:] \ {[0,0]}
and A9:
(
z in REAL+ &
z <> 0 )
;
* (x,(* (y,z))) = * ((* (x,y)),z)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
;
verum end; suppose that A22:
x in [:{0},REAL+:] \ {[0,0]}
and A23:
(
y in REAL+ &
y <> 0 )
and A24:
(
z in REAL+ &
z <> 0 )
;
* (x,(* (y,z))) = * ((* (x,y)),z)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
;
verum 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 )
;
* (x,(* (y,z))) = * ((* (x,y)),z)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
;
verum end; suppose that A49:
(
x in REAL+ &
x <> 0 )
and A50:
(
y in REAL+ &
y <> 0 )
and A51:
z in [:{0},REAL+:] \ {[0,0]}
;
* (x,(* (y,z))) = * ((* (x,y)),z)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
;
verum 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]}
;
* (x,(* (y,z))) = * ((* (x,y)),z)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
;
verum 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]}
;
* (x,(* (y,z))) = * ((* (x,y)),z)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
;
verum 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]}
;
* (x,(* (y,z))) = * ((* (x,y)),z)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;
verum 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]} ) )
;
* (x,(* (y,z))) = * ((* (x,y)),z) 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;
verum end;