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

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

end;

suppose that A2: x in REAL+ and
A3: ( y in REAL+ & z in REAL+ ) ; :: thesis:

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

end;

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

consider y99, z99 being Element of REAL+ such that
A10: y = y99 and
A11: z = [0,z99] and
A12: + (y,z) = y99 - z99 by A8, A9, Def1;
consider x9, y9 being Element of REAL+ such that
A13: ( x = x9 & y = y9 ) and
A14: * (x,y) = x9 *' y9 by A7, A8, Def2;
consider x99, z9 being Element of REAL+ such that
A15: x = x99 and
A16: z = [0,z9] and
A17: * (x,z) = [0,(x99 *' z9)] by A7, A9, Def2;
* (x,z) in [:{0},REAL+:] by A17, Lm1;
then A18: ex xy9, xz9 being Element of REAL+ st
( * (x,y) = xy9 & * (x,z) = [0,xz9] & + ((* (x,y)),(* (x,z))) = xy9 - xz9 ) by A14, Def1;
A19: z9 = z99 by A16, A11, XTUPLE_0:1;

now :: thesis:

per cases ;

suppose A20: z99 <=' y99 ; :: thesis:

then A21: + (y,z) = y99 -' z99 by A12, ARYTM_1:def 2;
then ex x999, yz9 being Element of REAL+ st
( x = x999 & + (y,z) = yz9 & * (x,(+ (y,z))) = x999 *' yz9 ) by A7, Def2;
hence * (x,(+ (y,z))) = (x9 *' y9) - (x99 *' z9) by A13, A15, A10, A19, A20, A21, ARYTM_1:26
.= + ((* (x,y)),(* (x,z))) by A14, A17, A18, XTUPLE_0:1 ;
:: thesis:

end;

suppose A22: not z99 <=' y99 ; :: thesis:

then A23: + (y,z) = [0,(z99 -' y99)] by A12, ARYTM_1:def 2;
then + (y,z) in [:{0},REAL+:] by Lm1;
then consider x999, yz9 being Element of REAL+ such that
A24: x = x999 and
A25: ( + (y,z) = [0,yz9] & * (x,(+ (y,z))) = [0,(x999 *' yz9)] ) by A7, Def2;
thus * (x,(+ (y,z))) = [0,(x999 *' (z99 -' y99))] by A23, A25, XTUPLE_0:1
.= (x9 *' y9) - (x99 *' z9) by A7, A13, A15, A10, A19, A22, A24, ARYTM_1:27
.= + ((* (x,y)),(* (x,z))) by A14, A17, A18, XTUPLE_0:1 ; :: thesis:

end;

hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; :: thesis:

end;

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

consider z99, y99 being Element of REAL+ such that
A29: z = z99 and
A30: y = [0,y99] and
A31: + (z,y) = z99 - y99 by A27, A28, Def1;
consider x9, z9 being Element of REAL+ such that
A32: ( x = x9 & z = z9 ) and
A33: * (x,z) = x9 *' z9 by A26, A27, Def2;
consider x99, y9 being Element of REAL+ such that
A34: x = x99 and
A35: y = [0,y9] and
A36: * (x,y) = [0,(x99 *' y9)] by A26, A28, Def2;
* (x,y) in [:{0},REAL+:] by A36, Lm1;
then A37: ex xz9, xy9 being Element of REAL+ st
( * (x,z) = xz9 & * (x,y) = [0,xy9] & + ((* (x,z)),(* (x,y))) = xz9 - xy9 ) by A33, Def1;
A38: y9 = y99 by A35, A30, XTUPLE_0:1;

now :: thesis:

per cases ;

suppose A39: y99 <=' z99 ; :: thesis:

then A40: + (z,y) = z99 -' y99 by A31, ARYTM_1:def 2;
then ex x999, zy9 being Element of REAL+ st
( x = x999 & + (z,y) = zy9 & * (x,(+ (z,y))) = x999 *' zy9 ) by A26, Def2;
hence * (x,(+ (z,y))) = (x9 *' z9) - (x99 *' y9) by A32, A34, A29, A38, A39, A40, ARYTM_1:26
.= + ((* (x,z)),(* (x,y))) by A33, A36, A37, XTUPLE_0:1 ;
:: thesis:

end;

suppose A41: not y99 <=' z99 ; :: thesis:

then A42: + (z,y) = [0,(y99 -' z99)] by A31, ARYTM_1:def 2;
then + (z,y) in [:{0},REAL+:] by Lm1;
then consider x999, zy9 being Element of REAL+ such that
A43: x = x999 and
A44: ( + (z,y) = [0,zy9] & * (x,(+ (z,y))) = [0,(x999 *' zy9)] ) by A26, Def2;
thus * (x,(+ (z,y))) = [0,(x999 *' (y99 -' z99))] by A42, A44, XTUPLE_0:1
.= (x9 *' z9) - (x99 *' y9) by A26, A32, A34, A29, A38, A41, A43, ARYTM_1:27
.= + ((* (x,z)),(* (x,y))) by A33, A36, A37, XTUPLE_0:1 ; :: thesis:

end;

hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; :: thesis:

end;

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

( ( not y in REAL+ or not z in [:{0},REAL+:] ) & ( not y in [:{0},REAL+:] or not z in REAL+ ) ) by A46, A47, Th5, XBOOLE_0:3;
then consider y99, z99 being Element of REAL+ such that
A48: y = [0,y99] and
A49: z = [0,z99] and
A50: + (y,z) = [0,(y99 + z99)] by A46, Def1;
+ (y,z) in [:{0},REAL+:] by A50, Lm1;
then consider x999, yz9 being Element of REAL+ such that
A51: x = x999 and
A52: ( + (y,z) = [0,yz9] & * (x,(+ (y,z))) = [0,(x999 *' yz9)] ) by A45, Def2;
consider x9, y9 being Element of REAL+ such that
A53: x = x9 and
A54: y = [0,y9] and
A55: * (x,y) = [0,(x9 *' y9)] by A45, A46, Def2;
A56: y9 = y99 by A54, A48, XTUPLE_0:1;
consider x99, z9 being Element of REAL+ such that
A57: x = x99 and
A58: z = [0,z9] and
A59: * (x,z) = [0,(x99 *' z9)] by A45, A47, Def2;
* (x,z) in [:{0},REAL+:] by A59, Lm1;
then A60: ( not * (x,y) in [:{0},REAL+:] or not * (x,z) in REAL+ ) by Th5, XBOOLE_0:3;
* (x,y) in [:{0},REAL+:] by A55, Lm1;
then ( not * (x,y) in REAL+ or not * (x,z) in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider xy9, xz9 being Element of REAL+ such that
A61: * (x,y) = [0,xy9] and
A62: ( * (x,z) = [0,xz9] & + ((* (x,y)),(* (x,z))) = [0,(xy9 + xz9)] ) by A55, A60, Def1, Lm1;
A63: xy9 = x9 *' y9 by A55, A61, XTUPLE_0:1;
A64: z9 = z99 by A58, A49, XTUPLE_0:1;
thus * (x,(+ (y,z))) = [0,(x999 *' (y99 + z99))] by A50, A52, XTUPLE_0:1
.= [0,((x9 *' y9) + (x9 *' z9))] by A53, A51, A56, A64, ARYTM_2:13
.= + ((* (x,y)),(* (x,z))) by A53, A57, A59, A62, A63, XTUPLE_0:1 ; :: thesis:

end;

suppose that A65: x in [:{0},REAL+:] \ {[0,0]} and
A66: y in REAL+ and
A67: z in REAL+ ; :: thesis:

consider y99, z99 being Element of REAL+ such that
A68: y = y99 and
A69: z = z99 and
A70: + (y,z) = y99 + z99 by A66, A67, Def1;

now :: thesis:

per cases ;

suppose that A71: y <> 0 and
A72: z <> 0 ; :: thesis:

consider x99, z9 being Element of REAL+ such that
A73: x = [0,x99] and
A74: z = z9 and
A75: * (x,z) = [0,(z9 *' x99)] by A65, A67, A72, Def2;
y99 + z99 <> 0 by A69, A72, ARYTM_2:5;
then consider x999, yz9 being Element of REAL+ such that
A76: x = [0,x999] and
A77: ( + (y,z) = yz9 & * (x,(+ (y,z))) = [0,(yz9 *' x999)] ) by A65, A70, Def2;
consider x9, y9 being Element of REAL+ such that
A78: x = [0,x9] and
A79: y = y9 and
A80: * (x,y) = [0,(y9 *' x9)] by A65, A66, A71, Def2;
A81: x99 = x999 by A73, A76, XTUPLE_0:1;
* (x,z) in [:{0},REAL+:] by A75, Lm1;
then A82: ( not * (x,y) in [:{0},REAL+:] or not * (x,z) in REAL+ ) by Th5, XBOOLE_0:3;
* (x,y) in [:{0},REAL+:] by A80, Lm1;
then ( not * (x,y) in REAL+ or not * (x,z) in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider xy9, xz9 being Element of REAL+ such that
A83: * (x,y) = [0,xy9] and
A84: ( * (x,z) = [0,xz9] & + ((* (x,y)),(* (x,z))) = [0,(xy9 + xz9)] ) by A80, A82, Def1, Lm1;
A85: xy9 = x9 *' y9 by A80, A83, XTUPLE_0:1;
x9 = x99 by A78, A73, XTUPLE_0:1;
hence * (x,(+ (y,z))) = [0,((x9 *' y9) + (x99 *' z9))] by A68, A69, A70, A79, A74, A77, A81, ARYTM_2:13
.= + ((* (x,y)),(* (x,z))) by A75, A84, A85, XTUPLE_0:1 ;
:: thesis:

end;

suppose A86: x = 0 ; :: thesis:

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

end;

suppose A87: z = 0 ; :: thesis:

hence * (x,(+ (y,z))) = * (x,y) by Th11
.= + ((* (x,y)),(* (x,z))) by A87, Th11, Th12 ;
:: thesis:

end;

suppose A88: y = 0 ; :: thesis:

hence * (x,(+ (y,z))) = * (x,z) by Th11
.= + ((* (x,y)),(* (x,z))) by A88, Th11, Th12 ;
:: thesis:

end;

hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; :: thesis:

end;

suppose that A89: x in [:{0},REAL+:] \ {[0,0]} and
A90: y in REAL+ and
A91: z in [:{0},REAL+:] \ {[0,0]} ; :: thesis:

consider x99, z9 being Element of REAL+ such that
A92: x = [0,x99] and
A93: z = [0,z9] and
A94: * (x,z) = z9 *' x99 by A89, A91, Def2;

now :: thesis:

per cases ;

suppose y <> 0 ; :: thesis:

then consider x9, y9 being Element of REAL+ such that
A95: x = [0,x9] and
A96: y = y9 and
A97: * (x,y) = [0,(y9 *' x9)] by A89, A90, Def2;
* (x,y) in [:{0},REAL+:] by A97, Lm1;
then consider xy9, xz9 being Element of REAL+ such that
A98: * (x,y) = [0,xy9] and
A99: ( * (x,z) = xz9 & + ((* (x,y)),(* (x,z))) = xz9 - xy9 ) by A94, Def1;
consider y99, z99 being Element of REAL+ such that
A100: y = y99 and
A101: z = [0,z99] and
A102: + (y,z) = y99 - z99 by A91, A96, Def1;
A103: z9 = z99 by A93, A101, XTUPLE_0:1;

now :: thesis:

per cases ;

suppose A104: z99 <=' y99 ; :: thesis:

then A105: + (y,z) = y99 -' z99 by A102, ARYTM_1:def 2;

now :: thesis:

per cases ;

suppose A106: + (y,z) <> 0 ; :: thesis:

then consider x999, yz9 being Element of REAL+ such that
A107: x = [0,x999] and
A108: ( + (y,z) = yz9 & * (x,(+ (y,z))) = [0,(yz9 *' x999)] ) by A89, A105, Def2;
not x in {[0,0]} by XBOOLE_0:def 5;
then A109: x999 <> 0 by A107, TARSKI:def 1;
A110: z9 = z99 by A93, A101, XTUPLE_0:1;
A111: x9 = x99 by A92, A95, XTUPLE_0:1;
x99 = x999 by A92, A107, XTUPLE_0:1;
hence * (x,(+ (y,z))) = (x9 *' z9) - (x9 *' y9) by A96, A100, A104, A105, A106, A108, A111, A110, A109, ARYTM_1:28
.= + ((* (x,y)),(* (x,z))) by A94, A97, A98, A99, A111, XTUPLE_0:1 ;
:: thesis:

end;

suppose A112: + (y,z) = 0 ; :: thesis:

then A113: y99 = z99 by A104, A105, ARYTM_1:10;
A114: ( xy9 = x9 *' y9 & x9 = x99 ) by A92, A95, A97, A98, XTUPLE_0:1;
thus * (x,(+ (y,z))) = 0 by A112, Th12
.= + ((* (x,y)),(* (x,z))) by A94, A96, A100, A99, A103, A113, A114, ARYTM_1:18 ; :: thesis:

end;

hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; :: thesis:

end;

suppose A115: not z99 <=' y99 ; :: thesis:

then A116: + (y,z) = [0,(z99 -' y99)] by A102, ARYTM_1:def 2;
then + (y,z) in [:{0},REAL+:] by Lm1;
then consider x999, yz9 being Element of REAL+ such that
A117: x = [0,x999] and
A118: ( + (y,z) = [0,yz9] & * (x,(+ (y,z))) = yz9 *' x999 ) by A89, Def2;
A119: x99 = x999 by A92, A117, XTUPLE_0:1;
A120: x9 = x99 by A92, A95, XTUPLE_0:1;
thus * (x,(+ (y,z))) = x999 *' (z99 -' y99) by A116, A118, XTUPLE_0:1
.= (x99 *' z9) - (x9 *' y9) by A96, A100, A103, A115, A120, A119, ARYTM_1:26
.= + ((* (x,y)),(* (x,z))) by A94, A97, A98, A99, XTUPLE_0:1 ; :: thesis:

end;

hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; :: thesis:

end;

suppose A121: y = 0 ; :: thesis:

hence * (x,(+ (y,z))) = * (x,z) by Th11
.= + ((* (x,y)),(* (x,z))) by A121, Th11, Th12 ;
:: thesis:

end;

hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; :: thesis:

end;

suppose that A122: x in [:{0},REAL+:] \ {[0,0]} and
A123: z in REAL+ and
A124: y in [:{0},REAL+:] \ {[0,0]} ; :: thesis:

consider x99, y9 being Element of REAL+ such that
A125: x = [0,x99] and
A126: y = [0,y9] and
A127: * (x,y) = y9 *' x99 by A122, A124, Def2;

now :: thesis:

per cases ;

suppose z <> 0 ; :: thesis:

then consider x9, z9 being Element of REAL+ such that
A128: x = [0,x9] and
A129: z = z9 and
A130: * (x,z) = [0,(z9 *' x9)] by A122, A123, Def2;
* (x,z) in [:{0},REAL+:] by A130, Lm1;
then consider xz9, xy9 being Element of REAL+ such that
A131: * (x,z) = [0,xz9] and
A132: ( * (x,y) = xy9 & + ((* (x,z)),(* (x,y))) = xy9 - xz9 ) by A127, Def1;
consider z99, y99 being Element of REAL+ such that
A133: z = z99 and
A134: y = [0,y99] and
A135: + (z,y) = z99 - y99 by A124, A129, Def1;
A136: y9 = y99 by A126, A134, XTUPLE_0:1;

now :: thesis:

per cases ;

suppose A137: y99 <=' z99 ; :: thesis:

then A138: + (z,y) = z99 -' y99 by A135, ARYTM_1:def 2;

now :: thesis:

per cases ;

suppose A139: + (z,y) <> 0 ; :: thesis:

then consider x999, zy9 being Element of REAL+ such that
A140: x = [0,x999] and
A141: ( + (z,y) = zy9 & * (x,(+ (z,y))) = [0,(zy9 *' x999)] ) by A122, A138, Def2;
not x in {[0,0]} by XBOOLE_0:def 5;
then A142: x999 <> 0 by A140, TARSKI:def 1;
A143: y9 = y99 by A126, A134, XTUPLE_0:1;
A144: x9 = x99 by A125, A128, XTUPLE_0:1;
x99 = x999 by A125, A140, XTUPLE_0:1;
hence * (x,(+ (z,y))) = (x9 *' y9) - (x9 *' z9) by A129, A133, A137, A138, A139, A141, A144, A143, A142, ARYTM_1:28
.= + ((* (x,z)),(* (x,y))) by A127, A130, A131, A132, A144, XTUPLE_0:1 ;
:: thesis:

end;

suppose A145: + (z,y) = 0 ; :: thesis:

then A146: z99 = y99 by A137, A138, ARYTM_1:10;
A147: ( xz9 = x9 *' z9 & x9 = x99 ) by A125, A128, A130, A131, XTUPLE_0:1;
thus * (x,(+ (z,y))) = 0 by A145, Th12
.= + ((* (x,z)),(* (x,y))) by A127, A129, A133, A132, A136, A146, A147, ARYTM_1:18 ; :: thesis:

end;

hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; :: thesis:

end;

suppose A148: not y99 <=' z99 ; :: thesis:

then A149: + (z,y) = [0,(y99 -' z99)] by A135, ARYTM_1:def 2;
then + (z,y) in [:{0},REAL+:] by Lm1;
then consider x999, zy9 being Element of REAL+ such that
A150: x = [0,x999] and
A151: ( + (z,y) = [0,zy9] & * (x,(+ (z,y))) = zy9 *' x999 ) by A122, Def2;
A152: x99 = x999 by A125, A150, XTUPLE_0:1;
A153: x9 = x99 by A125, A128, XTUPLE_0:1;
thus * (x,(+ (y,z))) = x999 *' (y99 -' z99) by A149, A151, XTUPLE_0:1
.= (x99 *' y9) - (x9 *' z9) by A129, A133, A136, A148, A153, A152, ARYTM_1:26
.= + ((* (x,y)),(* (x,z))) by A127, A130, A131, A132, XTUPLE_0:1 ; :: thesis:

end;

hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; :: thesis:

end;

suppose A154: z = 0 ; :: thesis:

hence * (x,(+ (y,z))) = * (x,y) by Th11
.= + ((* (x,y)),(* (x,z))) by A154, Th11, Th12 ;
:: thesis:

end;

hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; :: thesis:

end;

suppose that A155: x in [:{0},REAL+:] \ {[0,0]} and
A156: y in [:{0},REAL+:] \ {[0,0]} and
A157: z in [:{0},REAL+:] \ {[0,0]} ; :: thesis:

( ( not y in REAL+ or not z in [:{0},REAL+:] ) & ( not y in [:{0},REAL+:] or not z in REAL+ ) ) by A156, A157, Th5, XBOOLE_0:3;
then consider y99, z99 being Element of REAL+ such that
A158: y = [0,y99] and
A159: z = [0,z99] and
A160: + (y,z) = [0,(y99 + z99)] by A156, Def1;
consider x99, z9 being Element of REAL+ such that
A161: x = [0,x99] and
A162: z = [0,z9] and
A163: * (x,z) = z9 *' x99 by A155, A157, Def2;
A164: z9 = z99 by A162, A159, XTUPLE_0:1;
consider x9, y9 being Element of REAL+ such that
A165: x = [0,x9] and
A166: y = [0,y9] and
A167: * (x,y) = y9 *' x9 by A155, A156, Def2;
A168: y9 = y99 by A166, A158, XTUPLE_0:1;
+ (y,z) in [:{0},REAL+:] by A160, Lm1;
then consider x999, yz9 being Element of REAL+ such that
A169: x = [0,x999] and
A170: ( + (y,z) = [0,yz9] & * (x,(+ (y,z))) = yz9 *' x999 ) by A155, Def2;
A171: x9 = x999 by A165, A169, XTUPLE_0:1;
A172: ( ex xy9, xz9 being Element of REAL+ st
( * (x,y) = xy9 & * (x,z) = xz9 & + ((* (x,y)),(* (x,z))) = xy9 + xz9 ) & x9 = x99 ) by A165, A167, A161, A163, Def1, XTUPLE_0:1;
thus * (x,(+ (y,z))) = x999 *' (y99 + z99) by A160, A170, XTUPLE_0:1
.= + ((* (x,y)),(* (x,z))) by A167, A163, A172, A171, A168, A164, ARYTM_2:13 ; :: thesis:

end;

suppose A173: ( ( not x in REAL+ or not y in REAL+ 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 REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in REAL+ or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in REAL+ 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 REAL+ ) & ( 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+ \ {[0,0]}) \/ ([:{0},REAL+:] \ {[0,0]}) by XBOOLE_1:42
.= REAL+ \/ ([:{0},REAL+:] \ {[0,0]}) by ARYTM_2:3, ZFMISC_1:57 ;
hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) by A173, XBOOLE_0:def 3; :: thesis:

end;