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 add-associative
let x be non trivial Element of F; :: thesis: for o being object st not o in [#] F holds
ExField (x,o) is add-associative
let o be object ; :: thesis: ( not o in [#] F implies ExField (x,o) is add-associative )
assume a1: not o in [#] F ; :: thesis: ExField (x,o) is add-associative
then A1: for a being Element of F holds a <> o ;
set C = carr (x,o);
set E = ExField (x,o);
set ADDR = the addF of F;
A2: [#] (ExField (x,o)) = carr (x,o) by Def8;

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

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

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

suppose A3: a = o ; :: thesis: (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 A4: b = o ; :: thesis: (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 ( the addF of F . (x,x) <> x or the addF of F . (x,x) = x ) ;

suppose A5: the addF of F . (x,x) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A6: a + b = (addR (x,o)) . (a1,b1) by Def8
.= addR (a1,b1) by Def5
.= x + x by A3, A4, A5, Def4 ;
not x + x in {x} by A5, TARSKI:def 1;
then x + x in ([#] F) \ {x} by XBOOLE_0:def 5;
then reconsider xx = x + x as Element of carr (x,o) by XBOOLE_0:def 3;
A7: xx <> o by a1;

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

suppose A8: c = o ; :: thesis: (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;
A9: (a + b) + c = (addR (x,o)) . ((a + b),c1) by Def8
.= addR (xx,c1) by A6, Def5 ;
A10: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= x + x by A4, A5, A8, Def4 ;

per cases ( the addF of F . (xx,x) <> x or the addF of F . (xx,x) = x ) ;

suppose A11: the addF of F . (xx,x) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A12: the addF of F . (x,xx) = x + (x + x)
.= (x + x) + x ;
thus (a + b) + c = (x + x) + x by A1, A8, A9, A11, Def4
.= addR (a1,xx) by A1, A3, A11, A12, Def4
.= (addR (x,o)) . (a1,xx) by Def5
.= a + (b + c) by A10, Def8 ; :: thesis: verum

end;

suppose A13: the addF of F . (xx,x) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A14: the addF of F . (x,xx) = x + (x + x)
.= (x + x) + x ;
thus (a + b) + c = o by A7, A8, A9, A13, Def4
.= addR (a1,xx) by A3, A7, A13, A14, Def4
.= (addR (x,o)) . (a1,xx) by Def5
.= a + (b + c) by A10, Def8 ; :: thesis: verum

end;

end;

end;

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

then not c in {o} by TARSKI:def 1;
then c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
then reconsider cR = c as Element of F ;
reconsider c1 = c as Element of carr (x,o) by Def8;
A16: (a + b) + c = (addR (x,o)) . ((a + b),c1) by Def8
.= addR (xx,c1) by A6, Def5 ;
A17: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5 ;
then reconsider bc = b + c as Element of carr (x,o) ;

per cases ( the addF of F . (x,c1) <> x or the addF of F . (x,c1) = x ) ;

suppose A18: the addF of F . (x,c1) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

then A19: b + c = x + cR by A4, A15, A17, Def4;
then A20: b + c <> o by a1;

per cases ( the addF of F . (xx,c1) <> x or the addF of F . (xx,c1) = x ) ;

suppose the addF of F . (xx,c1) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

then A21: (a + b) + c = (x + x) + cR by A7, A15, A16, Def4
.= x + (x + cR) by RLVECT_1:def 3
.= the addF of F . (x,(b + c)) by A4, A15, A17, A18, Def4 ;

per cases ( the addF of F . (x,bc) <> x or the addF of F . (x,bc) = x ) ;

suppose the addF of F . (x,bc) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

hence (a + b) + c = addR (a1,bc) by A1, A3, A19, A21, Def4
.= (addR (x,o)) . (a1,(b + c)) by Def5
.= a + (b + c) by Def8 ;
:: thesis: verum

end;

suppose A22: the addF of F . (x,bc) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A23: the addF of F . (x,bc) = x + (x + cR) by A4, A15, A17, A18, Def4
.= (x + x) + cR by RLVECT_1:def 3
.= the addF of F . (xx,c1) ;
thus (a + b) + c = o by A7, A15, A16, A22, A23, Def4
.= addR (a1,bc) by A3, A20, A22, Def4
.= (addR (x,o)) . (a1,(b + c)) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

suppose A24: the addF of F . (xx,c1) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

then A25: (a + b) + c = o by A7, A15, A16, Def4;

per cases ( the addF of F . (x,bc) <> x or the addF of F . (x,bc) = x ) ;

suppose the addF of F . (x,bc) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A26: the addF of F . (x,bc) = x + (x + cR) by A4, A15, A17, A18, Def4
.= (x + x) + cR by RLVECT_1:def 3
.= the addF of F . (xx,c1) ;
thus (a + b) + c = addR (a1,bc) by A3, A20, A26, A24, A25, Def4
.= (addR (x,o)) . (a1,(b + c)) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A27: the addF of F . (x,bc) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

the addF of F . (x,bc) = x + (x + cR) by A4, A15, A17, A18, Def4
.= (x + x) + cR by RLVECT_1:def 3
.= the addF of F . (xx,c1) ;
hence (a + b) + c = o by A7, A15, A16, A27, Def4
.= addR (a1,bc) by A3, A20, A27, Def4
.= (addR (x,o)) . (a1,(b + c)) by Def5
.= a + (b + c) by Def8 ;
:: thesis: verum

end;

end;

end;

end;

end;

suppose A29: the addF of F . (x,c1) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

then x + cR = x ;
then A30: c1 = 0. F by RLVECT_1:9;
A31: b + c = o by A4, A29, A15, A17, Def4;

per cases ( the addF of F . (xx,c1) <> x or the addF of F . (xx,c1) = x ) ;

suppose the addF of F . (xx,c1) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

hence (a + b) + c = (x + x) + cR by A7, A15, A16, Def4
.= addR (a1,bc) by A3, A5, A30, A31, Def4
.= (addR (x,o)) . (a1,(b + c)) by Def5
.= a + (b + c) by Def8 ;
:: thesis: verum

end;

suppose the addF of F . (xx,c1) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

then x = (x + x) + cR
.= x + x by A30 ;
hence (a + b) + c = a + (b + c) by A5; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose A33: the addF of F . (x,x) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A34: a + b = (addR (x,o)) . (a1,b1) by Def8
.= addR (a1,b1) by Def5
.= o by A3, A4, A33, Def4 ;
then a + b in {o} by TARSKI:def 1;
then reconsider ab = a + b as Element of carr (x,o) by XBOOLE_0:def 3;

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

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

hence (a + b) + c = a + (b + c) by A3; :: thesis: verum

end;

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

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

per cases ( the addF of F . (x,c1) = x or the addF of F . (x,c1) <> x ) ;

suppose A37: the addF of F . (x,c1) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A38: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A4, A36, A37, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc = b + c as Element of carr (x,o) by XBOOLE_0:def 3;
thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A36, A34, A37, Def4
.= addR (a1,bc) by A3, A33, A38, Def4
.= (addR (x,o)) . (a1,(b + c)) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A39: the addF of F . (x,c1) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A40: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= x + cR by A4, A36, A39, Def4 ;
reconsider bc = b + c as Element of carr (x,o) by Def8;
A41: (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= the addF of F . (x,c1) by A34, A36, A39, Def4 ;
(a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= (x + x) + cR by A33, A34, A36, A39, Def4
.= x + (x + cR) by RLVECT_1:def 3
.= the addF of F . (x,bc) by A40 ;
hence (a + b) + c = addR (a1,bc) by A1, A3, A39, A40, A41, Def4
.= (addR (x,o)) . (a1,(b + c)) by Def5
.= a + (b + c) by Def8 ;
:: thesis: verum

end;

end;

end;

end;

end;

end;

end;

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

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

per cases ( the addF of F . (x,b) <> x or the addF of F . (x,b) = x ) ;

suppose A44: the addF of F . (x,b) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A45: a + b = (addR (x,o)) . (a1,b1) by Def8
.= addR (a1,b1) by Def5
.= x + bR by A3, A42, A44, Def4 ;
then A46: a + b <> o by A1;
then not a + b in {o} by TARSKI:def 1;
then a + b in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
then reconsider abR = a + b as Element of F ;
reconsider ab = a + b as Element of carr (x,o) by Def8;

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

suppose A47: c = o ; :: thesis: (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;
A48: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= bR + x by A42, A43, A44, A47, Def4 ;
A49: b + c <> o by A1, A48;
then not b + c in {o} by TARSKI:def 1;
then b + c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
then reconsider bcR = b + c as Element of F ;
reconsider bc = b + c as Element of carr (x,o) by Def8;
A50: the addF of F . (ab,x) = (x + bR) + x by A45
.= x + (bR + x) ;

per cases ( the addF of F . (ab,x) <> x or the addF of F . (ab,x) = x ) ;

suppose A51: the addF of F . (ab,x) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= the addF of F . (x,bc) by A1, A3, A47, A48, A50, A51, Def4
.= addR (a1,bc) by A1, A3, A48, A50, A51, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A52: the addF of F . (ab,x) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A46, A47, A52, Def4
.= addR (a1,bc) by A3, A48, A49, A50, A52, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

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

then not c in {o} by TARSKI:def 1;
then c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
then reconsider cR = c as Element of F ;
reconsider c1 = c as Element of carr (x,o) by Def8;
A54: the addF of F . (ab,c) = (x + bR) + cR by A45
.= x + (bR + cR) by RLVECT_1:def 3 ;

per cases ( the addF of F . (b,c) <> x or the addF of F . (b,c) = x ) ;

suppose A55: the addF of F . (b,c) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

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

per cases ( the addF of F . (ab,c1) <> x or the addF of F . (ab,c1) = x ) ;

suppose A58: the addF of F . (ab,c1) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= (x + bR) + cR by A45, A58, A53, A46, Def4
.= x + (bR + cR) by RLVECT_1:def 3
.= addR (a1,bc) by A1, A3, A54, A58, A56, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A59: the addF of F . (ab,c1) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A59, A53, A46, Def4
.= addR (a1,bc) by A3, A54, A59, A56, A57, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

suppose A60: the addF of F . (b,c) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A61: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A60, A53, A42, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc = b + c as Element of carr (x,o) by XBOOLE_0:def 3;

per cases ( the addF of F . (ab,c1) <> x or the addF of F . (ab,c1) = x ) ;

suppose A62: the addF of F . (ab,c1) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= (x + bR) + cR by A45, A46, A53, A62, Def4
.= x + (bR + cR) by RLVECT_1:def 3
.= addR (a1,bc) by A60, A3, A54, A62, A61, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A63: the addF of F . (ab,c1) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A63, A53, A46, Def4
.= addR (a1,bc) by A60, A3, A54, A63, A61, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose A64: the addF of F . (x,b) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A65: a + b = (addR (x,o)) . (a1,b1) by Def8
.= addR (a1,b1) by Def5
.= o by A64, A42, A3, Def4 ;
then a + b in {o} by TARSKI:def 1;
then reconsider ab = a + b as Element of carr (x,o) by XBOOLE_0:def 3;

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

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

hence (a + b) + c = a + (b + c) by A3; :: thesis: verum

end;

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

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

A70: now :: thesis: not the addF of F . (b,c) = x

assume the addF of F . (b,c) = x ; :: thesis: contradiction
then bR + cR = x + bR by A64
.= bR + x ;
then x = cR by ALGSTR_0:def 4;
then c in {x} by TARSKI:def 1;
hence contradiction by A69, XBOOLE_0:def 5; :: thesis: verum

end;

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

per cases ( the addF of F . (x,c1) <> x or the addF of F . (x,c1) = x ) ;

suppose A75: the addF of F . (x,c1) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= the addF of F . (x,c1) by A65, A75, A68, Def4
.= addR (a1,bc) by A74, A3, A75, A72, A1, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A76: the addF of F . (x,c1) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A76, A68, A65, Def4
.= addR (a1,bc) by A73, A76, A74, A3, A72, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

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

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

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

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

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

per cases ( the addF of F . (a1,x) = x or the addF of F . (a1,x) <> x ) ;

suppose A80: the addF of F . (a1,x) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A81: a + b = (addR (x,o)) . (a1,b1) by Def8
.= addR (a1,b1) by Def5
.= o by A80, A79, A77, Def4 ;
then a + b in {o} by TARSKI:def 1;
then reconsider ab = a + b as Element of carr (x,o) by XBOOLE_0:def 3;

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

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

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

per cases ( the addF of F . (x,x) = x or the addF of F . (x,x) <> x ) ;

suppose A82: the addF of F . (x,x) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A83: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A81a, A79, A82, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc = b + c as Element of carr (x,o) by XBOOLE_0:def 3;
thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A81, A81a, A82, Def4
.= addR (a1,bc) by A80, A77, A83, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A84: the addF of F . (x,x) <> x ; :: thesis: b₁ + (b₂ + b₃) = (b₁ + b₂) + b₃

A85: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= x + x by A84, A79, A81a, Def4 ;
then A86: b + c <> o by A1;
then not b + c in {o} by TARSKI:def 1;
then A87: b + c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider bcR = b + c as Element of F by A87;
reconsider bc = b + c as Element of carr (x,o) by Def8;
A88: (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= (aR + x) + x by A80, A81, A81a, A84, Def4 ;

now :: thesis: not the addF of F . (a1,bc) = x

assume the addF of F . (a1,bc) = x ; :: thesis: contradiction
then aR + bcR = aR + x by A80;
then bcR = x by ALGSTR_0:def 4;
then b + c in {x} by TARSKI:def 1;
hence contradiction by A87, XBOOLE_0:def 5; :: thesis: verum

end;

then the addF of F . (a1,bc) = addR (a1,bc) by A77, A86, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ;
hence a + (b + c) = aR + (x + x) by A85
.= (a + b) + c by A88, RLVECT_1:def 3 ;
:: thesis: verum

end;

end;

end;

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

not c in {o} by A90, TARSKI:def 1;
then A91: 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 A91;

per cases ( the addF of F . (x,c) = x or the addF of F . (x,c) <> x ) ;

suppose A92: the addF of F . (x,c) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A93: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A92, A90, A79, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc = b + c as Element of carr (x,o) by XBOOLE_0:def 3;
thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A81, A90, A92, Def4
.= addR (a1,bc) by A80, A77, A93, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A94: the addF of F . (x,c) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A95: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= x + cR by A94, A90, A79, Def4 ;
then A96: b + c <> o by A1;
then not b + c in {o} by TARSKI:def 1;
then A97: b + c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider bc = b + c as Element of carr (x,o) by Def8;
reconsider bcR = b + c as Element of F by A97;

A98: now :: thesis: not the addF of F . (a1,bc) = x

assume the addF of F . (a1,bc) = x ; :: thesis: contradiction
then aR + bcR = aR + x by A80;
then bcR = x by ALGSTR_0:def 4;
then b + c in {x} by TARSKI:def 1;
hence contradiction by A97, XBOOLE_0:def 5; :: thesis: verum

end;

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= (aR + x) + cR by A80, A81, A90, A94, Def4
.= aR + (x + cR) by RLVECT_1:def 3
.= addR (a1,bc) by A98, A96, A77, A95, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

suppose A100: the addF of F . (a1,x) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A101: a + b = (addR (x,o)) . (a1,b1) by Def8
.= addR (a1,b1) by Def5
.= aR + x by A79, A77, A100, Def4 ;
then A102: a + b <> o by A1;
then not a + b in {o} by TARSKI:def 1;
then A103: a + b in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider ab = a + b as Element of carr (x,o) by Def8;
reconsider abR = a + b as Element of F by A103;

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

suppose A104: c = o ; :: thesis: (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 ( the addF of F . (x,x) = x or the addF of F . (x,x) <> x ) ;

suppose A105: the addF of F . (x,x) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A106: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A105, A104, A79, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc = b + c as Element of carr (x,o) by XBOOLE_0:def 3;

A107: now :: thesis: not the addF of F . (ab,x) = x

assume the addF of F . (ab,x) = x ; :: thesis: contradiction
then x = (aR + x) + x by A101
.= aR + (x + x) by RLVECT_1:def 3
.= aR + x by A105 ;
hence contradiction by A100; :: thesis: verum

end;

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= (aR + x) + x by A101, A1, A104, A107, Def4
.= aR + (x + x) by RLVECT_1:def 3
.= addR (a1,bc) by A105, A100, A77, A106, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A109: the addF of F . (x,x) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A110: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= x + x by A109, A104, A79, Def4 ;
then A111: b + c <> o by A1;
then not b + c in {o} by TARSKI:def 1;
then A112: b + c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider bc = b + c as Element of carr (x,o) by Def8;
reconsider bcR = b + c as Element of F by A112;
A113: the addF of F . (a,bc) = aR + (x + x) by A110
.= (aR + x) + x by RLVECT_1:def 3
.= the addF of F . (ab,x) by A101 ;

per cases ( the addF of F . (ab,x) = x or the addF of F . (ab,x) <> x ) ;

suppose A114: the addF of F . (ab,x) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A102, A104, A114, Def4
.= addR (a1,bc) by A114, A77, A113, A111, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A115: the addF of F . (ab,x) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= the addF of F . (ab,x) by A101, A1, A104, A115, Def4
.= addR (a1,bc) by A115, A77, A113, A111, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

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

then not c in {o} by TARSKI:def 1;
then A117: 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 A117;

per cases ( the addF of F . (x,c) = x or the addF of F . (x,c) <> x ) ;

suppose A118: the addF of F . (x,c) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A119: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A118, A116, A79, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc = b + c as Element of carr (x,o) by XBOOLE_0:def 3;
A120: the addF of F . (ab,c) = (aR + x) + cR by A101
.= aR + (x + cR) by RLVECT_1:def 3
.= the addF of F . (a,x) by A118 ;

per cases ( the addF of F . (ab,c1) = x or the addF of F . (ab,c1) <> x ) ;

suppose A121: the addF of F . (ab,c1) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A102, A116, A121, Def4
.= addR (a1,bc) by A121, A77, A119, A120, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A122: the addF of F . (ab,c1) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= (aR + x) + cR by A101, A102, A116, A122, Def4
.= aR + (x + cR) by RLVECT_1:def 3
.= addR (a1,bc) by A119, A100, A77, A118, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

suppose A123: the addF of F . (x,c) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A124: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= x + cR by A123, A116, A79, Def4 ;
then A125: b + c <> o by A1;
then not b + c in {o} by TARSKI:def 1;
then A126: b + c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider bc = b + c as Element of carr (x,o) by Def8;
reconsider bcR = b + c as Element of F by A126;
A127: the addF of F . (a,bc) = aR + (x + cR) by A124
.= (aR + x) + cR by RLVECT_1:def 3
.= the addF of F . (ab,c) by A101 ;

per cases ( the addF of F . (ab,c1) = x or the addF of F . (ab,c1) <> x ) ;

suppose A128: the addF of F . (ab,c1) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A102, A116, A128, Def4
.= addR (a1,bc) by A128, A77, A125, A127, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A129: the addF of F . (ab,c1) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= (aR + x) + cR by A101, A102, A116, A129, Def4
.= aR + (x + cR) by RLVECT_1:def 3
.= addR (a1,bc) by A129, A77, A124, A127, A125, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

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

then not b in {o} by TARSKI:def 1;
then A131: 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 A131;

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

per cases ( the addF of F . (a,b) = x or the addF of F . (a,b) <> x ) ;

suppose A134: the addF of F . (a,b) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A135: a + b = (addR (x,o)) . (a1,b1) by Def8
.= addR (a1,b1) by Def5
.= o by A134, A130, A77, Def4 ;
then a + b in {o} by TARSKI:def 1;
then reconsider ab = a + b as Element of carr (x,o) by XBOOLE_0:def 3;

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

assume bR + x = x ; :: thesis: contradiction
then A138: bR + x = aR + bR by A134
.= bR + aR ;
x = aR by A138, ALGSTR_0:def 4;
then a in {x} by TARSKI:def 1;
hence contradiction by A78, XBOOLE_0:def 5; :: thesis: verum

end;

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

suppose A139: c = o ; :: thesis: (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: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= bR + x by A136, A139, A130, Def4 ;
then A141: b + c <> o by A1;
then not b + c in {o} by TARSKI:def 1;
then A142: b + c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider bc = b + c as Element of carr (x,o) by Def8;
reconsider bcR = b + c as Element of F by A142;

A143: now :: thesis: not the addF of F . (a,bc) = x

assume the addF of F . (a,bc) = x ; :: thesis: contradiction
then x = aR + (bR + x) by A140
.= (aR + bR) + x by RLVECT_1:def 3
.= x + x by A134 ;
hence contradiction by A132; :: thesis: verum

end;

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= (aR + bR) + x by A134, A135, A139, A132, Def4
.= aR + (bR + x) by RLVECT_1:def 3
.= addR (a1,bc) by A77, A141, A140, A143, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

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

then not c in {o} by TARSKI:def 1;
then A146: 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 A146;

per cases ( the addF of F . (b,c) <> x or the addF of F . (b,c) = x ) ;

suppose A147: the addF of F . (b,c) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A148: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= bR + cR by A145, A130, A147, Def4 ;
then A149: b + c <> o by A1;
not b + c in {o} by A149, TARSKI:def 1;
then A150: b + c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider bc = b + c as Element of carr (x,o) by Def8;
reconsider bcR = b + c as Element of F by A150;

per cases ( the addF of F . (x,c) <> x or the addF of F . (x,c) = x ) ;

suppose A151: the addF of F . (x,c) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A152: now :: thesis: not the addF of F . (a,bc) = x

assume the addF of F . (a,bc) = x ; :: thesis: contradiction
then x = aR + (bR + cR) by A148
.= (aR + bR) + cR by RLVECT_1:def 3
.= x + cR by A134 ;
hence contradiction by A151; :: thesis: verum

end;

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= (aR + bR) + cR by A134, A135, A145, A151, Def4
.= aR + (bR + cR) by RLVECT_1:def 3
.= addR (a1,bc) by A77, A148, A149, A152, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A154: the addF of F . (x,c) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A155: aR + (bR + cR) = (aR + bR) + cR by RLVECT_1:def 3
.= x by A134, A154 ;
thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A154, A135, A145, Def4
.= addR (a1,bc) by A155, A77, A149, A148, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

suppose A156: the addF of F . (b,c) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

then A157: bR + cR = aR + bR by A134
.= bR + aR ;
A158: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A130, A145, A156, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc = b + c as Element of carr (x,o) by XBOOLE_0:def 3;
A159: x + cR = aR + x by A157, ALGSTR_0:def 4
.= the addF of F . (a,x) ;

per cases ( the addF of F . (x,c) <> x or the addF of F . (x,c) = x ) ;

suppose A160: the addF of F . (x,c) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= x + cR by A135, A145, A160, Def4
.= addR (a1,bc) by A77, A159, A160, A158, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A161: the addF of F . (x,c) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A135, A145, A161, Def4
.= addR (a1,bc) by A77, A159, A161, A158, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose A162: the addF of F . (a,b) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A163: a + b = (addR (x,o)) . (a1,b1) by Def8
.= addR (a1,b1) by Def5
.= aR + bR by A162, A130, A77, Def4 ;
then A164: a + b <> o by A1;
then not a + b in {o} by TARSKI:def 1;
then A165: a + b in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider ab = a + b as Element of carr (x,o) by Def8;
reconsider abR = a + b as Element of F by A165;

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

suppose A166: c = o ; :: thesis: (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 ( the addF of F . (b,x) <> x or the addF of F . (b,x) = x ) ;

suppose A167: the addF of F . (b,x) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A168: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= bR + x by A166, A130, A167, Def4 ;
then A169: b + c <> o by A1;
then not b + c in {o} by TARSKI:def 1;
then A170: b + c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider bc = b + c as Element of carr (x,o) by Def8;
reconsider bcR = b + c as Element of F by A170;
A171: the addF of F . (ab,x) = (aR + bR) + x by A163
.= aR + (bR + x) by RLVECT_1:def 3
.= the addF of F . (a,bc) by A168 ;

per cases ( the addF of F . (ab,x) <> x or the addF of F . (ab,x) = x ) ;

suppose A172: the addF of F . (ab,x) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= (aR + bR) + x by A1, A163, A166, A172, Def4
.= aR + (bR + x) by RLVECT_1:def 3
.= addR (a1,bc) by A77, A168, A169, A171, A172, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A173: the addF of F . (ab,x) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A164, A166, A173, Def4
.= addR (a1,bc) by A77, A173, A169, A171, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

suppose A174: the addF of F . (b,x) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A175: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A166, A130, A174, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc = b + c as Element of carr (x,o) by XBOOLE_0:def 3;
A176: (aR + bR) + x = aR + (bR + x) by RLVECT_1:def 3
.= the addF of F . (a,x) by A174 ;

per cases ( the addF of F . (ab,x) <> x or the addF of F . (ab,x) = x ) ;

suppose A177: the addF of F . (ab,x) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= (aR + bR) + x by A163, A1, A166, A177, Def4
.= addR (a1,bc) by A163, A77, A177, A175, A176, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A178: the addF of F . (ab,x) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A164, A166, A178, Def4
.= addR (a1,bc) by A163, A77, A178, A175, A176, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

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

then not c in {o} by TARSKI:def 1;
then A180: 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 A180;

per cases ( the addF of F . (b,c) <> x or the addF of F . (b,c) = x ) ;

suppose A181: the addF of F . (b,c) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A182: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= bR + cR by A179, A130, A181, Def4 ;
then A183: b + c <> o by A1;
then not b + c in {o} by TARSKI:def 1;
then A184: b + c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;
reconsider bc = b + c as Element of carr (x,o) by Def8;
reconsider bcR = b + c as Element of F by A184;
A185: the addF of F . (ab,c) = (aR + bR) + cR by A163
.= aR + (bR + cR) by RLVECT_1:def 3
.= the addF of F . (a,bc) by A182 ;

per cases ( the addF of F . (ab,c) <> x or the addF of F . (ab,c) = x ) ;

suppose A186: the addF of F . (ab,c) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= (aR + bR) + cR by A163, A164, A179, A186, Def4
.= aR + (bR + cR) by RLVECT_1:def 3
.= addR (a1,bc) by A183, A77, A186, A182, A185, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A187: the addF of F . (ab,c) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A164, A179, A187, Def4
.= addR (a1,bc) by A183, A77, A187, A185, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

suppose A188: the addF of F . (b,c) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

A189: b + c = (addR (x,o)) . (b1,c1) by Def8
.= addR (b1,c1) by Def5
.= o by A130, A179, A188, Def4 ;
then b + c in {o} by TARSKI:def 1;
then reconsider bc = b + c as Element of carr (x,o) by XBOOLE_0:def 3;
A190: (aR + bR) + cR = aR + (bR + cR) by RLVECT_1:def 3
.= the addF of F . (a,x) by A188 ;

per cases ( the addF of F . (ab,c) <> x or the addF of F . (ab,c) = x ) ;

suppose A191: the addF of F . (ab,c) <> x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= (aR + bR) + cR by A163, A164, A179, A191, Def4
.= addR (a1,bc) by A77, A163, A189, A190, A191, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

suppose A192: the addF of F . (ab,c) = x ; :: thesis: (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

thus (a + b) + c = (addR (x,o)) . (ab,c1) by Def8
.= addR (ab,c1) by Def5
.= o by A164, A179, A192, Def4
.= addR (a1,bc) by A163, A77, A192, A189, A190, Def4
.= (addR (x,o)) . (a,bc) by Def5
.= a + (b + c) by Def8 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

hence ExField (x,o) is add-associative by RLVECT_1:def 3; :: thesis: verum