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;

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)

hence
ExField (x,o) is add-associative
by RLVECT_1:def 3; :: thesis: verumlet a, b, c be Element of (ExField (x,o)); :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

end;

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

end;

suppose A5:
the addF of F . (x,x) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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;

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

end;

suppose A8:
c = o
; :: thesis: (b_{1} + b_{2}) + 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;

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 ;

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

end;

suppose A11:
the addF of F . (xx,x) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A13:
the addF of F . (xx,x) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

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

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

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

end;

suppose A18:
the addF of F . (x,c1) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

then A19:
b + c = x + cR
by A4, A15, A17, Def4;

then A20: b + c <> o by a1;

end;then A20: b + c <> o by a1;

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

end;

suppose
the addF of F . (xx,c1) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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 ;

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

end;

suppose
the addF of F . (x,bc) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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;.= (addR (x,o)) . (a1,(b + c)) by Def5

.= a + (b + c) by Def8 ;

:: thesis: verum

suppose A22:
the addF of F . (x,bc) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A24:
the addF of F . (xx,c1) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

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

end;

suppose
the addF of F . (x,bc) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A27:
the addF of F . (x,bc) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A29:
the addF of F . (x,c1) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

then
x + cR = x
;

then A30: c1 = 0. F by RLVECT_1:9;

A31: b + c = o by A4, A29, A15, A17, Def4;

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

end;

suppose A33:
the addF of F . (x,x) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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;

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

end;

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

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;

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

end;

suppose A37:
the addF of F . (x,c1) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A39:
the addF of F . (x,c1) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

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

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

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

end;

suppose A44:
the addF of F . (x,b) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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;

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

end;

suppose A47:
c = o
; :: thesis: (b_{1} + b_{2}) + 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;

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

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

end;

suppose A51:
the addF of F . (ab,x) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A52:
the addF of F . (ab,x) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

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

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 ;

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

end;

suppose A55:
the addF of F . (b,c) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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;

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

end;

suppose A58:
the addF of F . (ab,c1) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A59:
the addF of F . (ab,c1) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A60:
the addF of F . (b,c) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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;

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

end;

suppose A62:
the addF of F . (ab,c1) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A63:
the addF of F . (ab,c1) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A64:
the addF of F . (x,b) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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;

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

end;

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

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;

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

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

A72: b + c =
(addR (x,o)) . (b1,c1)
by Def8
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;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

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

end;

suppose A75:
the addF of F . (x,c1) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A76:
the addF of F . (x,c1) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

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

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;

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

end;

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

b in {o}
by A79, 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
( the addF of F . (a1,x) = x or the addF of F . (a1,x) <> x )
;

end;

suppose A80:
the addF of F . (a1,x) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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;

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

end;

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

c in {o}
by A81a, 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
( the addF of F . (x,x) = x or the addF of F . (x,x) <> x )
;

end;

suppose A82:
the addF of F . (x,x) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A84:
the addF of F . (x,x) <> x
; :: thesis: b_{1} + (b_{2} + b_{3}) = (b_{1} + b_{2}) + b_{3}

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 ;

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

then the addF of F . (a1,bc) =
addR (a1,bc)
by A77, A86, Def4
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 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

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

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

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;

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

end;

suppose A92:
the addF of F . (x,c) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A94:
the addF of F . (x,c) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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;

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

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

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

suppose A100:
the addF of F . (a1,x) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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;

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

end;

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

end;

suppose A105:
the addF of F . (x,x) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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;

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

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

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

suppose A109:
the addF of F . (x,x) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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 ;

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

end;

suppose A114:
the addF of F . (ab,x) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A115:
the addF of F . (ab,x) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

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

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;

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

end;

suppose A118:
the addF of F . (x,c) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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 ;

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

end;

suppose A121:
the addF of F . (ab,c1) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A122:
the addF of F . (ab,c1) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A123:
the addF of F . (x,c) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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 ;

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

end;

suppose A128:
the addF of F . (ab,c1) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A129:
the addF of F . (ab,c1) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

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

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;

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

hence contradiction by Def2; :: thesis: verum

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

end;

suppose A134:
the addF of F . (a,b) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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;

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

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

end;

suppose A139:
c = o
; :: thesis: (b_{1} + b_{2}) + 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: 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;

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

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

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

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

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;

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

end;

suppose A147:
the addF of F . (b,c) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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;

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

end;

suppose A151:
the addF of F . (x,c) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

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

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

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

suppose A154:
the addF of F . (x,c) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A156:
the addF of F . (b,c) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

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

end;

suppose A160:
the addF of F . (x,c) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A161:
the addF of F . (x,c) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A162:
the addF of F . (a,b) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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;

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

end;

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

end;

suppose A167:
the addF of F . (b,x) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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 ;

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

end;

suppose A172:
the addF of F . (ab,x) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A173:
the addF of F . (ab,x) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A174:
the addF of F . (b,x) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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 ;

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

end;

suppose A177:
the addF of F . (ab,x) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A178:
the addF of F . (ab,x) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

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

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;

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

end;

suppose A181:
the addF of F . (b,c) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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 ;

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

end;

suppose A186:
the addF of F . (ab,c) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A187:
the addF of F . (ab,c) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A188:
the addF of F . (b,c) = x
; :: thesis: (b_{1} + b_{2}) + 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 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 ;

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

end;

suppose A191:
the addF of F . (ab,c) <> x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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

suppose A192:
the addF of F . (ab,c) = x
; :: thesis: (b_{1} + b_{2}) + b_{3} = b_{1} + (b_{2} + b_{3})

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