let F be non almost_trivial Field; :: thesis: for x being non trivial Element of F
for o being object st not o in [#] F holds
ExField (x,o) is distributive
let x be non trivial Element of F; :: thesis: for o being object st not o in [#] F holds
ExField (x,o) is distributive
let o be object ; :: thesis: ( not o in [#] F implies ExField (x,o) is distributive )
assume not o in [#] F ; :: thesis: ExField (x,o) is distributive
then A1: for a being Element of F holds a <> o ;
set C = carr (x,o);
set E = ExField (x,o);
A2: [#] (ExField (x,o)) = carr (x,o) by Def8;

A3: now :: thesis: not x + x = x

assume x + x = x ; :: thesis: contradiction
then x = 0. F by RLVECT_1:9;
hence contradiction by Def2; :: thesis: verum

end;

then not x + x in {x} by TARSKI:def 1;
then x + x in ([#] F) \ {x} by XBOOLE_0:def 5;
then reconsider xpx = x + x as Element of carr (x,o) by XBOOLE_0:def 3;
A4: x <> 0. F by Def2;
then A5: x is left_mult-cancelable by ALGSTR_0:def 36;

A6: now :: thesis: not x * x = x

assume x * x = x ; :: thesis: contradiction
then x * x = x * (1. F) ;
hence contradiction by A5, ALGSTR_0:def 20, Def2; :: thesis: verum

end;

then not x * x in {x} by TARSKI:def 1;
then x * x in ([#] F) \ {x} by XBOOLE_0:def 5;
then reconsider xmx = x * x as Element of carr (x,o) by XBOOLE_0:def 3;
A7: x * x <> o by A1;

A8: now :: thesis: not (x * x) + x = x

assume (x * x) + x = x ; :: thesis: contradiction
then x * x = 0. F by RLVECT_1:9;
then x = 0. F by VECTSP_2:def 1;
hence contradiction by Def2; :: thesis: verum

end;

then not (x * x) + x in {x} by TARSKI:def 1;
then (x * x) + x in ([#] F) \ {x} by XBOOLE_0:def 5;
then reconsider xmxpx = (x * x) + x as Element of carr (x,o) by XBOOLE_0:def 3;

A9: now :: thesis: for a, b, c being Element of (ExField (x,o)) holds (a * b) + (a * c) = a * (b + c)

let a, b, c be Element of (ExField (x,o)); :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

per cases ( a = o or a <> o ) ;

suppose A10: a = o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then a in {o} by TARSKI:def 1;
then reconsider a1 = a as Element of carr (x,o) by XBOOLE_0:def 3;

per cases ( b = o or b <> o ) ;

suppose A11: b = o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then b in {o} by TARSKI:def 1;
then reconsider b1 = b as Element of carr (x,o) by XBOOLE_0:def 3;
A12: a * b = (multR (x,o)) . (a1,b1) by Def8
.= multR (a1,b1) by Def7
.= x * x by A10, A11, A6, Def6 ;

per cases ( c = o or c <> o ) ;

suppose A13: c = o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then c in {o} by TARSKI:def 1;
then reconsider c1 = c as Element of carr (x,o) by XBOOLE_0:def 3;
A14: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= x + x by A13, A11, A3, Def4 ;
A15: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= x * x by A13, A10, A6, Def6 ;
A16: (x * x) + (x * x) = x * (x + x) by VECTSP_1:def 2;

per cases ( (x * x) + (x * x) <> x or (x * x) + (x * x) = x ) ;

suppose A17: (x * x) + (x * x) <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A18: ( xpx <> o & xmx <> o ) by A1;
thus (a * b) + (a * c) = (addR (x,o)) . (xmx,xmx) by A15, A12, Def8
.= addR (xmx,xmx) by Def5
.= (x * x) + (x * x) by A18, A17, Def4
.= multR (a1,xpx) by A1, A17, A10, A16, Def6
.= (multR (x,o)) . (a1,xpx) by Def7
.= a * (b + c) by A14, Def8 ; :: thesis: verum

end;

suppose A19: (x * x) + (x * x) = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A20: ( xpx <> o & xmx <> o ) by A1;
thus (a * b) + (a * c) = (addR (x,o)) . (xmx,xmx) by A15, A12, Def8
.= addR (xmx,xmx) by Def5
.= o by A20, A19, Def4
.= multR (a1,xpx) by A20, A19, A10, A16, Def6
.= (multR (x,o)) . (a1,xpx) by Def7
.= a * (b + c) by A14, Def8 ; :: thesis: verum

end;

end;

end;

suppose A21: c <> o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then not c in {o} by TARSKI:def 1;
then A22: c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider c1 = c as Element of carr (x,o) by Def8;
reconsider cR = c as Element of F by A22;

per cases ( x + cR = x or x + cR <> x ) ;

suppose A23: x + cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then A24: cR = 0. F by RLVECT_1:9;
A25: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A23, A21, A11, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc1 = b + c as Element of carr (x,o) by XBOOLE_0:def 3;
A26: x * cR <> x by A24, Def2;
A27: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= x * cR by A26, A21, A10, Def6 ;
then A28: a * c <> o by A1;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;

A29: now :: thesis: not (x * x) + (x * cR) = x

assume (x * x) + (x * cR) = x ; :: thesis: contradiction
then x * (x + cR) = x * (1. F) by VECTSP_1:def 2;
then x + cR = 1. F by A4, VECTSP_2:8;
hence contradiction by A23, Def2; :: thesis: verum

end;

thus (a * b) + (a * c) = (addR (x,o)) . (xmx,ac1) by A12, Def8
.= addR (xmx,ac1) by Def5
.= (x * x) + (x * cR) by A7, A28, A27, A29, Def4
.= x * x by A23, VECTSP_1:def 2
.= multR (a1,bc1) by A10, A25, A6, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A30: x + cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A31: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= x + cR by A30, A21, A11, Def4 ;
then A32: b + c <> o by A1;
then not b + c in {o} by TARSKI:def 1;
then A33: b + c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider bc1 = b + c as Element of carr (x,o) by Def8;
reconsider bcR = b + c as Element of F by A33;

per cases ( x * cR = x or x * cR <> x ) ;

suppose A34: x * cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A35: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= o by A34, A21, A10, Def6 ;
then a * c in {o} by TARSKI:def 1;
then reconsider ac1 = a * c as Element of carr (x,o) by XBOOLE_0:def 3;
A36: x * (x + cR) <> x by A34, A8, VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (xmx,ac1) by A12, Def8
.= addR (xmx,ac1) by Def5
.= (x * x) + x by A8, A1, A35, Def4
.= x * (x + cR) by A34, VECTSP_1:def 2
.= multR (a1,bc1) by A10, A31, A1, A36, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A37: x * cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A38: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= x * cR by A37, A21, A10, Def6 ;
then A39: a * c <> o by A1;
then not a * c in {o} by TARSKI:def 1;
then A40: a * c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;
reconsider acR = a * c as Element of F by A40;

per cases ( (x * x) + (x * cR) <> x or (x * x) + (x * cR) = x ) ;

suppose A41: (x * x) + (x * cR) <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then A42: x * (x + cR) <> x by VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (xmx,ac1) by A12, Def8
.= addR (xmx,ac1) by Def5
.= (x * x) + (x * cR) by A41, A7, A38, A39, Def4
.= x * (x + cR) by VECTSP_1:def 2
.= multR (a1,bc1) by A42, A10, A31, A1, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A43: (x * x) + (x * cR) = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then A44: x * (x + cR) = x by VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (xmx,ac1) by A12, Def8
.= addR (xmx,ac1) by Def5
.= o by A43, A7, A38, A39, Def4
.= multR (a1,bc1) by A44, A10, A31, A32, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

suppose A45: b <> o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then not b in {o} by TARSKI:def 1;
then A46: b in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider b1 = b as Element of carr (x,o) by Def8;
reconsider bR = b as Element of F by A46;

per cases ( x * bR = x or x * bR <> x ) ;

suppose A47: x * bR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A48: a * b = (multR (x,o)) . (a1,b1) by Def8
.= multR (a1,b1) by Def7
.= o by A10, A45, A47, Def6 ;
then a * b in {o} by TARSKI:def 1;
then reconsider ab1 = a * b as Element of carr (x,o) by XBOOLE_0:def 3;

per cases ( c = o or c <> o ) ;

suppose A49: c = o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then c in {o} by TARSKI:def 1;
then reconsider c1 = c as Element of carr (x,o) by XBOOLE_0:def 3;
A50: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= x * x by A10, A49, A6, Def6 ;

A51: now :: thesis: not bR + x = x

assume bR + x = x ; :: thesis: contradiction
then bR = 0. F by RLVECT_1:9;
hence contradiction by A47, Def2; :: thesis: verum

end;

A52: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= bR + x by A51, A49, A45, Def4 ;
then b + c <> o by A1;
then not b + c in {o} by TARSKI:def 1;
then A53: b + c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider bc1 = b + c as Element of carr (x,o) by Def8;
A54: x * (bR + x) = x + (x * x) by A47, VECTSP_1:def 2;
reconsider bcR = b + c as Element of F by A53;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,xmx) by A50, Def8
.= addR (ab1,xmx) by Def5
.= x + (x * x) by A8, A48, A1, Def4
.= multR (a1,bc1) by A10, A52, A8, A54, A1, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A55: c <> o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then not c in {o} by TARSKI:def 1;
then A56: c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider c1 = c as Element of carr (x,o) by Def8;
reconsider cR = c as Element of F by A56;

per cases ( bR + cR = x or bR + cR <> x ) ;

suppose A57: bR + cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A58: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A45, A55, A57, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc1 = b + c as Element of carr (x,o) by XBOOLE_0:def 3;

per cases ( x * cR = x or x * cR <> x ) ;

suppose A59: x * cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A60: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= o by A10, A55, A59, Def6 ;
then a * c in {o} by TARSKI:def 1;
then reconsider ac1 = a * c as Element of carr (x,o) by XBOOLE_0:def 3;
A61: x * x = x + x

proof

A62: x <> 0. F by Def2;
x * bR = x * (1. F) by A47;
then A63: bR = 1. F by A62, VECTSP_2:8;
A64: x * cR = x * (1. F) by A59;
A65: x = (1. F) + (1. F) by A57, A62, A63, A64, VECTSP_2:8;
hence x * x = ((1. F) * ((1. F) + (1. F))) + ((1. F) * ((1. F) + (1. F))) by VECTSP_1:def 3
.= x + x by A65 ;
:: thesis: verum

end;

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= x + x by A60, A48, A3, Def4
.= multR (a1,bc1) by A61, A10, A58, A6, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A66: x * cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A67: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= x * cR by A10, A55, A66, Def6 ;
then a * c <> o by A1;
then not a * c in {o} by TARSKI:def 1;
then A68: a * c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;
reconsider acR = a * c as Element of F by A68;
A69: x * x = x + (x * cR) by A47, A57, VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= x + (x * cR) by A1, A67, A48, A69, A6, Def4
.= multR (a1,bc1) by A69, A10, A58, A6, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

suppose A70: bR + cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A71: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= bR + cR by A45, A55, A70, Def4 ;
then A72: b + c <> o by A1;
then not b + c in {o} by TARSKI:def 1;
then A73: b + c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider bc1 = b + c as Element of carr (x,o) by Def8;
reconsider bcR = b + c as Element of F by A73;

per cases ( x * cR = x or x * cR <> x ) ;

suppose A74: x * cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A75: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= o by A10, A55, A74, Def6 ;
then a * c in {o} by TARSKI:def 1;
then reconsider ac1 = a * c as Element of carr (x,o) by XBOOLE_0:def 3;

A76: now :: thesis: not x * (bR + cR) = x

assume A77: x * (bR + cR) = x ; :: thesis: contradiction
A78: x <> 0. F by Def2;
x * (1. F) = (x * (1. F)) + (x * cR) by A47, A77, VECTSP_1:def 2
.= x * ((1. F) + cR) by VECTSP_1:def 2 ;
then 1. F = (1. F) + cR by A78, VECTSP_2:8;
then cR = 0. F by RLVECT_1:9;
hence contradiction by A74, Def2; :: thesis: verum

end;

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= x + x by A3, A75, A48, Def4
.= x * (bR + cR) by A74, A47, VECTSP_1:def 2
.= multR (a1,bc1) by A76, A10, A1, A71, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A79: x * cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A80: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= x * cR by A10, A55, A79, Def6 ;
then A81: a * c <> o by A1;
then not a * c in {o} by TARSKI:def 1;
then A82: a * c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;
reconsider acR = a * c as Element of F by A82;
A83: x * (bR + cR) = x + (x * cR) by A47, VECTSP_1:def 2;

per cases ( x + (x * cR) = x or x + (x * cR) <> x ) ;

suppose A84: x + (x * cR) = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A81, A80, A48, A84, Def4
.= multR (a1,bc1) by A84, A83, A10, A71, A72, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A85: x + (x * cR) <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= x + (x * cR) by A1, A80, A48, A85, Def4
.= multR (a1,bc1) by A85, A83, A10, A71, A1, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

suppose A86: x * bR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A87: a * b = (multR (x,o)) . (a1,b1) by Def8
.= multR (a1,b1) by Def7
.= x * bR by A10, A45, A86, Def6 ;
then A88: a * b <> o by A1;
then not a * b in {o} by TARSKI:def 1;
then A89: a * b in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider ab1 = a * b as Element of carr (x,o) by Def8;
reconsider abR = a * b as Element of F by A89;

per cases ( c = o or c <> o ) ;

suppose A90: c = o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then c in {o} by TARSKI:def 1;
then reconsider c1 = c as Element of carr (x,o) by XBOOLE_0:def 3;
A91: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= x * x by A10, A90, A6, Def6 ;
then A92: a * c <> o by A1;
then not a * c in {o} by TARSKI:def 1;
then A93: a * c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;
reconsider acR = a * c as Element of F by A93;

per cases ( bR + x = x or bR + x <> x ) ;

suppose A94: bR + x = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A95: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A45, A90, A94, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc1 = b + c as Element of carr (x,o) by XBOOLE_0:def 3;
A96: (x * bR) + (x * x) = x * x by A94, VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (x * bR) + (x * x) by A87, A88, A91, A92, A96, A6, Def4
.= multR (a1,bc1) by A10, A95, A96, A6, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A97: bR + x <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A98: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= bR + x by A45, A90, A97, Def4 ;
then A99: b + c <> o by A1;
then not b + c in {o} by TARSKI:def 1;
then A100: b + c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider bc1 = b + c as Element of carr (x,o) by Def8;
reconsider bcR = b + c as Element of F by A100;

per cases ( (x * bR) + (x * x) <> x or (x * bR) + (x * x) = x ) ;

suppose A101: (x * bR) + (x * x) <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A102: (x * bR) + (x * x) = x * (bR + x) by VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (x * bR) + (x * x) by A87, A88, A91, A92, A101, Def4
.= multR (a1,bc1) by A10, A98, A1, A101, A102, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A103: (x * bR) + (x * x) = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A104: (x * bR) + (x * x) = x * (bR + x) by VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A87, A88, A91, A92, A103, Def4
.= multR (a1,bc1) by A10, A98, A99, A103, A104, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

suppose A105: c <> o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then not c in {o} by TARSKI:def 1;
then A106: c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider c1 = c as Element of carr (x,o) by Def8;
reconsider cR = c as Element of F by A106;

per cases ( bR + cR = x or bR + cR <> x ) ;

suppose A107: bR + cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A108: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A45, A105, A107, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc1 = b + c as Element of carr (x,o) by XBOOLE_0:def 3;
A109: (x * bR) + (x * cR) = x * x by A107, VECTSP_1:def 2;

per cases ( x * cR <> x or x * cR = x ) ;

suppose A110: x * cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A111: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= x * cR by A10, A105, A110, Def6 ;
then A112: a * c <> o by A1;
then not a * c in {o} by TARSKI:def 1;
then A113: a * c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;
reconsider acR = a * c as Element of F by A113;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (x * bR) + (x * cR) by A87, A88, A111, A112, A109, A6, Def4
.= multR (a1,bc1) by A10, A108, A6, A109, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A114: x * cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A115: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= o by A10, A105, A114, Def6 ;
then a * c in {o} by TARSKI:def 1;
then reconsider ac1 = a * c as Element of carr (x,o) by XBOOLE_0:def 3;

A116: now :: thesis: not (x * bR) + x = x

assume (x * bR) + x = x ; :: thesis: contradiction
then A117: x * (1. F) = x * (bR + cR) by A114, VECTSP_1:def 2;
x <> 0. F by Def2;
then bR + cR = 1. F by A117, VECTSP_2:8;
hence contradiction by A107, Def2; :: thesis: verum

end;

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (x * bR) + x by A87, A1, A115, A116, Def4
.= multR (a1,bc1) by A10, A108, A6, A109, A114, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

suppose A118: bR + cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A119: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= bR + cR by A45, A105, A118, Def4 ;
then A120: b + c <> o by A1;
then not b + c in {o} by TARSKI:def 1;
then A121: b + c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider bc1 = b + c as Element of carr (x,o) by Def8;
reconsider bcR = b + c as Element of F by A121;
A122: (x * bR) + (x * cR) = x * (bR + cR) by VECTSP_1:def 2;

per cases ( x * cR <> x or x * cR = x ) ;

suppose A123: x * cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A124: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= x * cR by A10, A105, A123, Def6 ;
then A125: a * c <> o by A1;
then not a * c in {o} by TARSKI:def 1;
then A126: a * c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;
reconsider acR = a * c as Element of F by A126;

per cases ( (x * bR) + (x * cR) <> x or (x * bR) + (x * cR) = x ) ;

suppose A127: (x * bR) + (x * cR) <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (x * bR) + (x * cR) by A87, A88, A124, A125, A127, Def4
.= multR (a1,bc1) by A10, A119, A1, A127, A122, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A128: (x * bR) + (x * cR) = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A87, A88, A124, A125, A128, Def4
.= multR (a1,bc1) by A10, A119, A120, A128, A122, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

suppose A129: x * cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A130: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= o by A10, A105, A129, Def6 ;
then a * c in {o} by TARSKI:def 1;
then reconsider ac1 = a * c as Element of carr (x,o) by XBOOLE_0:def 3;
A131: (x * bR) + x = x * (bR + cR) by A129, VECTSP_1:def 2;

per cases ( (x * bR) + x <> x or (x * bR) + x = x ) ;

suppose A132: (x * bR) + x <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (x * bR) + x by A87, A1, A130, A132, Def4
.= multR (a1,bc1) by A10, A119, A1, A132, A131, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A133: (x * bR) + x = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A87, A88, A130, A133, Def4
.= multR (a1,bc1) by A10, A119, A120, A133, A131, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

suppose A134: a <> o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then not a in {o} by TARSKI:def 1;
then A135: a in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider a1 = a as Element of carr (x,o) by Def8;
reconsider aR = a as Element of [#] F by A135;

per cases ( b = o or b <> o ) ;

suppose A136: b = o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then b in {o} by TARSKI:def 1;
then reconsider b1 = b as Element of carr (x,o) by XBOOLE_0:def 3;

per cases ( aR * x = x or aR * x <> x ) ;

suppose A137: aR * x = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A138: a * b = (multR (x,o)) . (a1,b1) by Def8
.= multR (a1,b1) by Def7
.= o by A134, A136, A137, Def6 ;
then a * b in {o} by TARSKI:def 1;
then reconsider ab1 = a * b as Element of carr (x,o) by XBOOLE_0:def 3;

per cases ( c = o or c <> o ) ;

suppose A139: c = o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then c in {o} by TARSKI:def 1;
then reconsider c1 = c as Element of carr (x,o) by XBOOLE_0:def 3;
A140: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= o by A134, A139, A137, Def6 ;
then a * c in {o} by TARSKI:def 1;
then reconsider ac1 = a * c as Element of carr (x,o) by XBOOLE_0:def 3;
A141: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= x + x by A136, A139, A3, Def4 ;
then A142: b + c <> o by A1;
reconsider bc1 = b + c as Element of carr (x,o) by Def8;
A143: aR * (x + x) = x + x by A137, VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= x + x by A140, A138, A3, Def4
.= multR (a1,bc1) by A143, A142, A134, A141, A3, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A144: c <> o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then not c in {o} by TARSKI:def 1;
then A145: c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider c1 = c as Element of carr (x,o) by Def8;
reconsider cR = c as Element of [#] F by A145;

A146: now :: thesis: not aR * cR = x

assume A147: aR * cR = x ; :: thesis: contradiction
aR <> 0. F by A137, Def2;
then cR = x by A137, A147, VECTSP_2:8;
then cR in {x} by TARSKI:def 1;
hence contradiction by A145, XBOOLE_0:def 5; :: thesis: verum

end;

A148: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= aR * cR by A134, A144, A146, Def6 ;
then A149: a * c <> o by A1;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;

per cases ( x + cR = x or x + cR <> x ) ;

suppose A150: x + cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then A151: (aR * x) + (aR * cR) = aR * x by VECTSP_1:def 2;
A152: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A144, A136, A150, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc1 = b + c as Element of carr (x,o) by XBOOLE_0:def 3;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A137, A138, A148, A149, A151, Def4
.= multR (a1,bc1) by A134, A152, A137, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A153: x + cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A154: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= x + cR by A136, A144, A153, Def4 ;
then A155: b + c <> o by A1;
reconsider bc1 = b + c as Element of carr (x,o) by Def8;

A156: now :: thesis: not x + (aR * cR) = x

assume x + (aR * cR) = x ; :: thesis: contradiction
then A158: aR * x = aR * (x + cR) by A137, VECTSP_1:def 2;
aR <> 0. F by A137, Def2;
hence contradiction by A153, A158, VECTSP_2:8; :: thesis: verum

end;

A159: x + (aR * cR) = aR * (x + cR) by A137, VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= x + (aR * cR) by A138, A148, A1, A156, Def4
.= multR (a1,bc1) by A134, A154, A155, A156, A159, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

suppose A160: aR * x <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A161: a * b = (multR (x,o)) . (a1,b1) by Def8
.= multR (a1,b1) by Def7
.= aR * x by A134, A136, A160, Def6 ;
then A162: a * b <> o by A1;
then not a * b in {o} by TARSKI:def 1;
then A163: a * b in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider ab1 = a * b as Element of carr (x,o) by Def8;
reconsider abR = a * b as Element of F by A163;

per cases ( c = o or c <> o ) ;

suppose A164: c = o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then c in {o} by TARSKI:def 1;
then reconsider c1 = c as Element of carr (x,o) by XBOOLE_0:def 3;
A165: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= aR * x by A134, A164, A160, Def6 ;
then A166: a * c <> o by A1;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;
A167: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= x + x by A136, A164, A3, Def4 ;
then A168: b + c <> o by A1;
reconsider bc1 = b + c as Element of carr (x,o) by Def8;
A169: aR * (x + x) = (aR * x) + (aR * x) by VECTSP_1:def 2;

per cases ( (aR * x) + (aR * x) <> x or (aR * x) + (aR * x) = x ) ;

suppose A170: (aR * x) + (aR * x) <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (aR * x) + (aR * x) by A161, A165, A166, A170, Def4
.= multR (a1,bc1) by A134, A170, A169, A168, A167, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A171: (aR * x) + (aR * x) = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A161, A165, A166, A171, Def4
.= multR (a1,bc1) by A134, A171, A169, A168, A167, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

suppose A172: c <> o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then not c in {o} by TARSKI:def 1;
then A173: c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider c1 = c as Element of carr (x,o) by Def8;
reconsider cR = c as Element of [#] F by A173;

per cases ( aR * cR = x or aR * cR <> x ) ;

suppose A174: aR * cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A175: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= o by A134, A172, A174, Def6 ;
then a * c in {o} by TARSKI:def 1;
then reconsider ac1 = a * c as Element of carr (x,o) by XBOOLE_0:def 3;

per cases ( x + cR = x or x + cR <> x ) ;

suppose A176: x + cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A177: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A136, A172, A176, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc1 = b + c as Element of carr (x,o) by XBOOLE_0:def 3;
A178: (aR * x) + x = aR * x by A176, A174, VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (aR * x) + x by A160, A161, A1, A175, A178, Def4
.= multR (a1,bc1) by A134, A177, A178, A160, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A179: x + cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A180: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= x + cR by A136, A172, A179, Def4 ;
then A181: b + c <> o by A1;
reconsider bc1 = b + c as Element of carr (x,o) by Def8;
A182: (aR * x) + x = aR * (x + cR) by A174, VECTSP_1:def 2;

per cases ( (aR * x) + x <> x or (aR * x) + x = x ) ;

suppose A183: (aR * x) + x <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (aR * x) + x by A161, A1, A175, A183, Def4
.= multR (a1,bc1) by A134, A180, A181, A183, A182, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A184: (aR * x) + x = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A161, A162, A175, A184, Def4
.= multR (a1,bc1) by A134, A180, A181, A184, A182, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

suppose A185: aR * cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A186: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= aR * cR by A134, A172, A185, Def6 ;
then A187: a * c <> o by A1;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;

per cases ( x + cR = x or x + cR <> x ) ;

suppose A188: x + cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A189: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A136, A172, A188, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc1 = b + c as Element of carr (x,o) by XBOOLE_0:def 3;
A190: (aR * x) + (aR * cR) = aR * x by A188, VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (aR * x) + (aR * cR) by A160, A161, A162, A186, A187, A190, Def4
.= multR (a1,bc1) by A160, A134, A189, A190, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A191: x + cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A192: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= x + cR by A136, A172, A191, Def4 ;
then A193: b + c <> o by A1;
reconsider bc1 = b + c as Element of carr (x,o) by Def8;
A194: (aR * x) + (aR * cR) = aR * (x + cR) by VECTSP_1:def 2;

per cases ( (aR * x) + (aR * cR) = x or (aR * x) + (aR * cR) <> x ) ;

suppose A195: (aR * x) + (aR * cR) = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A161, A162, A186, A187, A195, Def4
.= multR (a1,bc1) by A134, A192, A193, A195, A194, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A196: (aR * x) + (aR * cR) <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (aR * x) + (aR * cR) by A161, A162, A186, A187, A196, Def4
.= multR (a1,bc1) by A134, A192, A193, A196, A194, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

suppose A197: b <> o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then not b in {o} by TARSKI:def 1;
then A198: b in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider b1 = b as Element of carr (x,o) by Def8;
reconsider bR = b as Element of [#] F by A198;

per cases ( aR * bR = x or aR * bR <> x ) ;

suppose A199: aR * bR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A200: a * b = (multR (x,o)) . (a1,b1) by Def8
.= multR (a1,b1) by Def7
.= o by A134, A197, A199, Def6 ;
then a * b in {o} by TARSKI:def 1;
then reconsider ab1 = a * b as Element of carr (x,o) by XBOOLE_0:def 3;
A201: aR * (bR + x) = x + (aR * x) by A199, VECTSP_1:def 2;

A202: now :: thesis: not bR + x = x

assume bR + x = x ; :: thesis: contradiction
then bR = 0. F by RLVECT_1:9;
hence contradiction by A199, Def2; :: thesis: verum

end;

A203: now :: thesis: not aR * x = x

assume aR * x = x ; :: thesis: contradiction
then A205: x * aR = x * (1. F) by GROUP_1:def 12;
x <> 0. F by Def2;
then aR = 1. F by A205, VECTSP_2:8;
then bR in {x} by A199, TARSKI:def 1;
hence contradiction by A198, XBOOLE_0:def 5; :: thesis: verum

end;

per cases ( c = o or c <> o ) ;

suppose A206: c = o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then c in {o} by TARSKI:def 1;
then reconsider c1 = c as Element of carr (x,o) by XBOOLE_0:def 3;
A207: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= bR + x by A197, A206, A202, Def4 ;
then A208: b + c <> o by A1;
reconsider bc1 = b + c as Element of carr (x,o) by Def8;
reconsider bcR = b + c as Element of F by A207;
A209: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= aR * x by A134, A206, A203, Def6 ;
then A210: a * c <> o by A1;
then not a * c in {o} by TARSKI:def 1;
then A211: a * c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;
reconsider acR = a * c as Element of F by A211;

per cases ( x + (aR * x) = x or x + (aR * x) <> x ) ;

suppose A212: x + (aR * x) = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A200, A209, A210, A212, Def4
.= multR (a1,bc1) by A201, A134, A207, A208, A212, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A213: x + (aR * x) <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= x + (aR * x) by A200, A209, A1, A213, Def4
.= multR (a1,bc1) by A201, A134, A207, A208, A213, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

suppose A214: c <> o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then not c in {o} by TARSKI:def 1;
then A215: c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider c1 = c as Element of carr (x,o) by Def8;
reconsider cR = c as Element of F by A215;

per cases ( bR + cR = x or bR + cR <> x ) ;

suppose A216: bR + cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A217: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A197, A214, A216, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc1 = b + c as Element of carr (x,o) by XBOOLE_0:def 3;

per cases ( aR * cR = x or aR * cR <> x ) ;

suppose A218: aR * cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A219: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= o by A134, A214, A218, Def6 ;
then a * c in {o} by TARSKI:def 1;
then reconsider ac1 = a * c as Element of carr (x,o) by XBOOLE_0:def 3;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= x + x by A200, A219, A3, Def4
.= aR * x by A216, A218, A199, VECTSP_1:def 2
.= multR (a1,bc1) by A134, A217, A203, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A220: aR * cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A221: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= aR * cR by A134, A214, A220, Def6 ;
then not a * c = o by A1;
then not a * c in {o} by TARSKI:def 1;
then A222: a * c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;
reconsider acR = a * c as Element of F by A222;
A223: x + (aR * cR) = aR * x by A216, A199, VECTSP_1:def 2;

per cases ( x + (aR * cR) = x or x + (aR * cR) <> x ) ;

suppose x + (aR * cR) = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

hence (a * b) + (a * c) = a * (b + c) by A203, A216, A199, VECTSP_1:def 2; :: thesis: verum

end;

suppose A225: x + (aR * cR) <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= x + (aR * cR) by A200, A221, A1, A225, Def4
.= multR (a1,bc1) by A134, A217, A225, A223, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

suppose A226: bR + cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A227: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= bR + cR by A197, A214, A226, Def4 ;
then A228: b + c <> o by A1;
reconsider bc1 = b + c as Element of carr (x,o) by Def8;

per cases ( aR * cR = x or aR * cR <> x ) ;

suppose A229: aR * cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A230: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= o by A134, A214, A229, Def6 ;
then a * c in {o} by TARSKI:def 1;
then reconsider ac1 = a * c as Element of carr (x,o) by XBOOLE_0:def 3;
A231: aR * (bR + cR) = x + x by A229, A199, VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= x + x by A200, A230, A3, Def4
.= multR (a1,bc1) by A3, A231, A134, A228, A227, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A232: aR * cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A233: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= aR * cR by A134, A214, A232, Def6 ;
then A234: not a * c = o by A1;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;
A235: x + (aR * cR) = aR * (bR + cR) by A199, VECTSP_1:def 2;

per cases ( x + (aR * cR) = x or x + (aR * cR) <> x ) ;

suppose A236: x + (aR * cR) = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A200, A233, A234, A236, Def4
.= multR (a1,bc1) by A134, A227, A228, A236, A235, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A237: x + (aR * cR) <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= x + (aR * cR) by A200, A233, A1, A237, Def4
.= multR (a1,bc1) by A134, A227, A228, A237, A235, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

suppose A238: aR * bR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A239: a * b = (multR (x,o)) . (a1,b1) by Def8
.= multR (a1,b1) by Def7
.= aR * bR by A134, A197, A238, Def6 ;
then A240: a * b <> o by A1;
reconsider ab1 = a * b as Element of carr (x,o) by Def8;
reconsider abR = a * b as Element of F by A239;

per cases ( c = o or c <> o ) ;

suppose A241: c = o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then c in {o} by TARSKI:def 1;
then reconsider c1 = c as Element of carr (x,o) by XBOOLE_0:def 3;

per cases ( bR + x <> x or bR + x = x ) ;

suppose A242: bR + x <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A243: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= bR + x by A197, A241, A242, Def4 ;
then A244: b + c <> o by A1;
reconsider bc1 = b + c as Element of carr (x,o) by Def8;

per cases ( aR * x <> x or aR * x = x ) ;

suppose A245: aR * x <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A246: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= aR * x by A134, A241, A245, Def6 ;
then A247: a * c <> o by A1;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;
A248: (aR * bR) + (aR * x) = aR * (bR + x) by VECTSP_1:def 2;

per cases ( (aR * bR) + (aR * x) <> x or (aR * bR) + (aR * x) = x ) ;

suppose A249: (aR * bR) + (aR * x) <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (aR * bR) + (aR * x) by A240, A239, A246, A247, A249, Def4
.= multR (a1,bc1) by A134, A243, A244, A249, A248, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A250: (aR * bR) + (aR * x) = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A240, A239, A246, A247, A250, Def4
.= multR (a1,bc1) by A134, A243, A244, A250, A248, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

suppose A251: aR * x = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A252: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= o by A134, A241, A251, Def6 ;
then a * c in {o} by TARSKI:def 1;
then reconsider ac1 = a * c as Element of carr (x,o) by XBOOLE_0:def 3;
A253: (aR * bR) + x = aR * (bR + x) by A251, VECTSP_1:def 2;

per cases ( (aR * bR) + x <> x or (aR * bR) + x = x ) ;

suppose A254: (aR * bR) + x <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (aR * bR) + x by A1, A239, A252, A254, Def4
.= multR (a1,bc1) by A134, A243, A244, A254, A253, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A255: (aR * bR) + x = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A240, A239, A252, A255, Def4
.= multR (a1,bc1) by A134, A243, A244, A255, A253, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

suppose A256: bR + x = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A257: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A197, A241, A256, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc1 = b + c as Element of carr (x,o) by XBOOLE_0:def 3;

per cases ( aR * x <> x or aR * x = x ) ;

suppose A258: aR * x <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A259: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= aR * x by A134, A241, A258, Def6 ;
then A260: a * c <> o by A1;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;
A261: (aR * bR) + (aR * x) = aR * x by A256, VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= aR * x by A240, A239, A259, A260, A258, A261, Def4
.= multR (a1,bc1) by A258, A134, A257, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A262: aR * x = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A263: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= o by A134, A241, A262, Def6 ;
then a * c in {o} by TARSKI:def 1;
then reconsider ac1 = a * c as Element of carr (x,o) by XBOOLE_0:def 3;
A264: (aR * bR) + x = x by A256, A262, VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A240, A239, A263, A264, Def4
.= multR (a1,bc1) by A262, A134, A257, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

suppose A265: c <> o ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then not c in {o} by TARSKI:def 1;
then A266: c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider c1 = c as Element of carr (x,o) by Def8;
reconsider cR = c as Element of F by A266;
A267: (aR * bR) + (aR * cR) = aR * (bR + cR) by VECTSP_1:def 2;

per cases ( bR + cR <> x or bR + cR = x ) ;

suppose A268: bR + cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A269: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= bR + cR by A197, A265, A268, Def4 ;
then A270: b + c <> o by A1;
reconsider bc1 = b + c as Element of carr (x,o) by Def8;

per cases ( aR * cR <> x or aR * cR = x ) ;

suppose A271: aR * cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A272: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= aR * cR by A134, A265, A271, Def6 ;
then A273: a * c <> o by A1;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;

per cases ( (aR * bR) + (aR * cR) <> x or (aR * bR) + (aR * cR) = x ) ;

suppose A274: (aR * bR) + (aR * cR) <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (aR * bR) + (aR * cR) by A240, A239, A272, A273, A274, Def4
.= multR (a1,bc1) by A134, A269, A270, A274, A267, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A275: (aR * bR) + (aR * cR) = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A240, A239, A272, A273, A275, Def4
.= multR (a1,bc1) by A134, A269, A270, A275, A267, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

suppose A276: aR * cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A277: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= o by A134, A265, A276, Def6 ;
then a * c in {o} by TARSKI:def 1;
then reconsider ac1 = a * c as Element of carr (x,o) by XBOOLE_0:def 3;

per cases ( (aR * bR) + x <> x or (aR * bR) + x = x ) ;

suppose A278: (aR * bR) + x <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

then A279: aR * (bR + cR) <> x by A276, VECTSP_1:def 2;
thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (aR * bR) + x by A1, A239, A277, A278, Def4
.= aR * (bR + cR) by A276, VECTSP_1:def 2
.= multR (a1,bc1) by A134, A269, A270, A279, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A280: (aR * bR) + x = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A240, A239, A277, A280, Def4
.= multR (a1,bc1) by A267, A276, A134, A269, A270, A280, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

suppose A281: bR + cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A282: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A197, A265, A281, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc1 = b + c as Element of carr (x,o) by XBOOLE_0:def 3;

per cases ( aR * cR <> x or aR * cR = x ) ;

suppose A283: aR * cR <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A284: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= aR * cR by A134, A265, A283, Def6 ;
then A285: a * c <> o by A1;
reconsider ac1 = a * c as Element of carr (x,o) by Def8;

per cases ( (aR * bR) + (aR * cR) <> x or (aR * bR) + (aR * cR) = x ) ;

suppose A286: (aR * bR) + (aR * cR) <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (aR * bR) + (aR * cR) by A240, A239, A284, A285, A286, Def4
.= multR (a1,bc1) by A286, A134, A281, A282, A267, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A287: (aR * bR) + (aR * cR) = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A240, A239, A284, A285, A287, Def4
.= multR (a1,bc1) by A287, A134, A281, A282, A267, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

suppose A288: aR * cR = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

A289: a * c = (multR (x,o)) . (a1,c1) by Def8
.= multR (a1,c1) by Def7
.= o by A134, A265, A288, Def6 ;
then a * c in {o} by TARSKI:def 1;
then reconsider ac1 = a * c as Element of carr (x,o) by XBOOLE_0:def 3;
A290: (aR * bR) + x = aR * (bR + cR) by A288, VECTSP_1:def 2;

per cases ( (aR * bR) + x <> x or (aR * bR) + x = x ) ;

suppose A291: (aR * bR) + x <> x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= (aR * bR) + x by A1, A239, A289, A291, Def4
.= multR (a1,bc1) by A291, A134, A281, A282, A290, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

suppose A292: (aR * bR) + x = x ; :: thesis: (b₁ * b₂) + (b₁ * b₃) = b₁ * (b₂ + b₃)

thus (a * b) + (a * c) = (addR (x,o)) . (ab1,ac1) by Def8
.= addR (ab1,ac1) by Def5
.= o by A240, A239, A289, A292, Def4
.= multR (a1,bc1) by A292, A134, A281, A282, A290, Def6
.= (multR (x,o)) . (a1,bc1) by Def7
.= a * (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

now :: thesis: for a, b, c being Element of (ExField (x,o)) holds
( a * (b + c) = (a * b) + (a * c) & (b + c) * a = (b * a) + (c * a) )

let a, b, c be Element of (ExField (x,o)); :: thesis: ( a * (b + c) = (a * b) + (a * c) & (b + c) * a = (b * a) + (c * a) )
thus a * (b + c) = (a * b) + (a * c) by A9; :: thesis: (b + c) * a = (b * a) + (c * a)
thus (b + c) * a = a * (b + c) by GROUP_1:def 12
.= (a * b) + (a * c) by A9
.= (b * a) + (a * c) by GROUP_1:def 12
.= (b * a) + (c * a) by GROUP_1:def 12 ; :: thesis: verum

end;

hence ExField (x,o) is distributive ; :: thesis: verum