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;

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;

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;

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;

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

then
not x + x in {x}
by TARSKI:def 1;assume
x + x = x
; :: thesis: contradiction

then x = 0. F by RLVECT_1:9;

hence contradiction by Def2; :: thesis: verum

end;then x = 0. F by RLVECT_1:9;

hence contradiction by Def2; :: thesis: verum

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

then
not x * x in {x}
by TARSKI:def 1;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 x * x = x * (1. F) ;

hence contradiction by A5, ALGSTR_0:def 20, Def2; :: thesis: verum

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

then
not (x * x) + x in {x}
by TARSKI:def 1;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 x * x = 0. F by RLVECT_1:9;

then x = 0. F by VECTSP_2:def 1;

hence contradiction by Def2; :: thesis: verum

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_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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

end;

suppose A10:
a = o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

then
a in {o}
by TARSKI:def 1;

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

end;then reconsider a1 = a as Element of carr (x,o) by XBOOLE_0:def 3;

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

end;

suppose A11:
b = o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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 ;

end;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 )
;

end;

suppose A13:
c = o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;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 )
;

end;

suppose A17:
(x * x) + (x * x) <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;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

suppose A19:
(x * x) + (x * x) = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;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

suppose A21:
c <> o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;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 )
;

end;

suppose A23:
x + cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

.= 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;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

thus (a * b) + (a * c) =
(addR (x,o)) . (xmx,ac1)
by A12, Def8
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;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

.= 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

suppose A30:
x + cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A34:
x * cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A37:
x * cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A41:
(x * x) + (x * cR) <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;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

suppose A43:
(x * x) + (x * cR) = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;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

suppose A45:
b <> o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;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 )
;

end;

suppose A47:
x * bR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A49:
c = o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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 ;

.= 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;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

A52: b + c =
(addR (x,o)) . (b1,c1)
by Def8
assume
bR + x = x
; :: thesis: contradiction

then bR = 0. F by RLVECT_1:9;

hence contradiction by A47, Def2; :: thesis: verum

end;then bR = 0. F by RLVECT_1:9;

hence contradiction by A47, Def2; :: thesis: verum

.= 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

suppose A55:
c <> o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;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 )
;

end;

suppose A57:
bR + cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A59:
x * cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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

.= 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;.= 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

thus (a * b) + (a * c) =
(addR (x,o)) . (ab1,ac1)
by Def8
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;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

.= 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

suppose A66:
x * cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A70:
bR + cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A74:
x * cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

.= 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;.= 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

thus (a * b) + (a * c) =
(addR (x,o)) . (ab1,ac1)
by Def8
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;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

.= 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

suppose A79:
x * cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A84:
x + (x * cR) = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A85:
x + (x * cR) <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A86:
x * bR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A90:
c = o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;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 )
;

end;

suppose A94:
bR + x = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A97:
bR + x <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A101:
(x * bR) + (x * x) <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;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

suppose A103:
(x * bR) + (x * x) = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;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

suppose A105:
c <> o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;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 )
;

end;

suppose A107:
bR + cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A110:
x * cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A114:
x * cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

.= 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;.= 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

thus (a * b) + (a * c) =
(addR (x,o)) . (ab1,ac1)
by Def8
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;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

.= 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

suppose A118:
bR + cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A123:
x * cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A127:
(x * bR) + (x * cR) <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A128:
(x * bR) + (x * cR) = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A129:
x * cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A132:
(x * bR) + x <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A133:
(x * bR) + x = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A134:
a <> o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;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 )
;

end;

suppose A136:
b = o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

then
b in {o}
by TARSKI:def 1;

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

end;then reconsider b1 = b as Element of carr (x,o) by XBOOLE_0:def 3;

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

end;

suppose A137:
aR * x = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A139:
c = o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;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

suppose A144:
c <> o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

.= 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;

end;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

A148: a * c =
(multR (x,o)) . (a1,c1)
by Def8
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;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

.= 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 )
;

end;

suppose A150:
x + cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;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

suppose A153:
x + cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

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;.= 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

A159:
x + (aR * cR) = aR * (x + cR)
by A137, VECTSP_1:def 2;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;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

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

suppose A160:
aR * x <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A164:
c = o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;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 )
;

end;

suppose A170:
(aR * x) + (aR * x) <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A171:
(aR * x) + (aR * x) = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A172:
c <> o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;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 )
;

end;

suppose A174:
aR * cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A176:
x + cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A179:
x + cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A183:
(aR * x) + x <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A184:
(aR * x) + x = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A185:
aR * cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A188:
x + cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A191:
x + cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A195:
(aR * x) + (aR * cR) = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A196:
(aR * x) + (aR * cR) <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A197:
b <> o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;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 )
;

end;

suppose A199:
aR * bR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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;then bR = 0. F by RLVECT_1:9;

hence contradiction by A199, Def2; :: thesis: verum

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;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

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

end;

suppose A206:
c = o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;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 )
;

end;

suppose A212:
x + (aR * x) = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A213:
x + (aR * x) <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A214:
c <> o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;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 )
;

end;

suppose A216:
bR + cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A218:
aR * cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A220:
aR * cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose
x + (aR * cR) = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

end;

end;

suppose A225:
x + (aR * cR) <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A226:
bR + cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A229:
aR * cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A232:
aR * cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A236:
x + (aR * cR) = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A237:
x + (aR * cR) <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A238:
aR * bR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A241:
c = o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

then
c in {o}
by TARSKI:def 1;

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

end;then reconsider c1 = c as Element of carr (x,o) by XBOOLE_0:def 3;

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

end;

suppose A242:
bR + x <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A245:
aR * x <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A249:
(aR * bR) + (aR * x) <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A250:
(aR * bR) + (aR * x) = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A251:
aR * x = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A254:
(aR * bR) + x <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A255:
(aR * bR) + x = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A256:
bR + x = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A258:
aR * x <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A262:
aR * x = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A265:
c <> o
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;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 )
;

end;

suppose A268:
bR + cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A271:
aR * cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A274:
(aR * bR) + (aR * cR) <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A275:
(aR * bR) + (aR * cR) = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A276:
aR * cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A278:
(aR * bR) + x <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;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

suppose A280:
(aR * bR) + x = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A281:
bR + cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A283:
aR * cR <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A286:
(aR * bR) + (aR * cR) <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A287:
(aR * bR) + (aR * cR) = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A288:
aR * cR = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;

end;.= 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 )
;

end;

suppose A291:
(aR * bR) + x <> x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

suppose A292:
(aR * bR) + x = x
; :: thesis: (b_{1} * b_{2}) + (b_{1} * b_{3}) = b_{1} * (b_{2} + b_{3})

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;.= 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

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) )

hence
ExField (x,o) is distributive
; :: thesis: verum( 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;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