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 associative

let x be non trivial Element of F; :: thesis: for o being object st not o in [#] F holds

ExField (x,o) is associative

let o be object ; :: thesis: ( not o in [#] F implies ExField (x,o) is associative )

assume not o in [#] F ; :: thesis: ExField (x,o) is associative

then A1: for a being Element of F holds a <> o ;

set C = carr (x,o);

set E = ExField (x,o);

set MULTR = the multF 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 associative

let x be non trivial Element of F; :: thesis: for o being object st not o in [#] F holds

ExField (x,o) is associative

let o be object ; :: thesis: ( not o in [#] F implies ExField (x,o) is associative )

assume not o in [#] F ; :: thesis: ExField (x,o) is associative

then A1: for a being Element of F holds a <> o ;

set C = carr (x,o);

set E = ExField (x,o);

set MULTR = the multF 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 associative
; :: 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 multF of F . (x,x) <> x or the multF of F . (x,x) = x )
;

end;

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

A6: a * b =
(multR (x,o)) . (a1,b1)
by Def8

.= multR (a1,b1) by Def7

.= x * x by A5, A4, A3, Def6 ;

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;.= multR (a1,b1) by Def7

.= x * x by A5, A4, A3, Def6 ;

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 = (multR (x,o)) . ((a * b),c1) by Def8

.= multR (xx,c1) by A6, Def7 ;

A10: b * c = (multR (x,o)) . (b1,c1) by Def8

.= multR (b1,c1) by Def7

.= x * x by A4, A5, A8, Def6 ;

A11: the multF of F . (x,xx) = x * (x * x)

.= (x * x) * x by GROUP_1:def 3 ;

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

A9: (a * b) * c = (multR (x,o)) . ((a * b),c1) by Def8

.= multR (xx,c1) by A6, Def7 ;

A10: b * c = (multR (x,o)) . (b1,c1) by Def8

.= multR (b1,c1) by Def7

.= x * x by A4, A5, A8, Def6 ;

A11: the multF of F . (x,xx) = x * (x * x)

.= (x * x) * x by GROUP_1:def 3 ;

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

end;

suppose A14:
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;

A15: (a * b) * c = (multR (x,o)) . ((a * b),c1) by Def8

.= multR (xx,c1) by A6, Def7 ;

A16: b * c = (multR (x,o)) . (b1,c1) by Def8

.= multR (b1,c1) by Def7 ;

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;

A15: (a * b) * c = (multR (x,o)) . ((a * b),c1) by Def8

.= multR (xx,c1) by A6, Def7 ;

A16: b * c = (multR (x,o)) . (b1,c1) by Def8

.= multR (b1,c1) by Def7 ;

then reconsider bc = b * c as Element of carr (x,o) ;

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

end;

suppose A17:
the multF of F . (x,c1) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

then A18:
b * c = x * cR
by A16, A14, A4, Def6;

then A19: b * c <> o by A1;

end;then A19: b * c <> o by A1;

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

end;

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

then A20: (a * b) * c =
(x * x) * cR
by A7, A15, A14, Def6

.= x * (x * cR) by GROUP_1:def 3

.= the multF of F . (x,(b * c)) by A17, A16, A14, A4, Def6 ;

end;.= x * (x * cR) by GROUP_1:def 3

.= the multF of F . (x,(b * c)) by A17, A16, A14, A4, Def6 ;

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

end;

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

hence (a * b) * c =
multR (a1,bc)
by A18, A1, A3, Def6, A20

.= (multR (x,o)) . (a1,(b * c)) by Def7

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

:: thesis: verum

end;.= (multR (x,o)) . (a1,(b * c)) by Def7

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

:: thesis: verum

suppose A21:
the multF of F . (x,bc) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A22: the multF of F . (x,bc) =
x * (x * cR)
by A17, A16, A14, A4, Def6

.= (x * x) * cR by GROUP_1:def 3

.= the multF of F . (xx,c1) ;

thus (a * b) * c = o by A15, A7, A14, A22, A21, Def6

.= multR (a1,bc) by A3, A19, A21, Def6

.= (multR (x,o)) . (a1,(b * c)) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= (x * x) * cR by GROUP_1:def 3

.= the multF of F . (xx,c1) ;

thus (a * b) * c = o by A15, A7, A14, A22, A21, Def6

.= multR (a1,bc) by A3, A19, A21, Def6

.= (multR (x,o)) . (a1,(b * c)) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A23:
the multF of F . (xx,c1) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

then A24:
(a * b) * c = o
by A7, A15, A14, Def6;

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

end;

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

A25: the multF of F . (x,bc) =
x * (x * cR)
by A17, A16, A14, A4, Def6

.= (x * x) * cR by GROUP_1:def 3

.= the multF of F . (xx,c1) ;

thus (a * b) * c = multR (a1,bc) by A25, A23, A19, A3, Def6, A24

.= (multR (x,o)) . (a1,(b * c)) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= (x * x) * cR by GROUP_1:def 3

.= the multF of F . (xx,c1) ;

thus (a * b) * c = multR (a1,bc) by A25, A23, A19, A3, Def6, A24

.= (multR (x,o)) . (a1,(b * c)) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A26:
the multF of F . (x,bc) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A27: the multF of F . (x,bc) =
x * (x * cR)
by A17, A16, A14, A4, Def6

.= (x * x) * cR by GROUP_1:def 3

.= the multF of F . (xx,c1) ;

thus (a * b) * c = o by A15, A7, A14, A27, A26, Def6

.= multR (a1,bc) by A19, A26, A3, Def6

.= (multR (x,o)) . (a1,(b * c)) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= (x * x) * cR by GROUP_1:def 3

.= the multF of F . (xx,c1) ;

thus (a * b) * c = o by A15, A7, A14, A27, A26, Def6

.= multR (a1,bc) by A19, A26, A3, Def6

.= (multR (x,o)) . (a1,(b * c)) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A28:
the multF of F . (x,c1) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A29:
x <> 0. F
by Def2;

A30: x = x * cR by A28

.= cR * x by GROUP_1:def 12 ;

A31: cR = cR * (1_ F)

.= cR * (x * (x ")) by A29, VECTSP_2:9

.= x * (x ") by A30, GROUP_1:def 3

.= 1_ F by A29, VECTSP_2:9 ;

A32: b * c = o by A28, A16, A14, A4, Def6;

end;A30: x = x * cR by A28

.= cR * x by GROUP_1:def 12 ;

A31: cR = cR * (1_ F)

.= cR * (x * (x ")) by A29, VECTSP_2:9

.= x * (x ") by A30, GROUP_1:def 3

.= 1_ F by A29, VECTSP_2:9 ;

A32: b * c = o by A28, A16, A14, A4, Def6;

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

end;

suppose A34:
the multF of F . (x,x) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A35: a * b =
(multR (x,o)) . (a1,b1)
by Def8

.= multR (a1,b1) by Def7

.= o by A34, A4, A3, Def6 ;

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;.= multR (a1,b1) by Def7

.= o by A34, A4, A3, Def6 ;

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

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

A37: b * c = (multR (x,o)) . (b1,c1) by Def8

.= multR (b1,c1) by Def7

.= o by A34, A36, A4, Def6 ;

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 = a * (b * c) by A35, A36, A37, A3; :: thesis: verum

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

A37: b * c = (multR (x,o)) . (b1,c1) by Def8

.= multR (b1,c1) by Def7

.= o by A34, A36, A4, Def6 ;

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 = a * (b * c) by A35, A36, A37, A3; :: thesis: verum

suppose A38:
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 multF of F . (x,c1) = x or the multF of F . (x,c1) <> x )
;

end;

suppose A39:
the multF of F . (x,c1) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A40: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= o by A39, A38, A4, Def6 ;

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 = (multR (x,o)) . (ab,c1) by Def8

.= multR (ab,c1) by Def7

.= o by A39, A35, A38, Def6

.= multR (a1,bc) by A40, A34, A3, Def6

.= (multR (x,o)) . (a1,(b * c)) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (b1,c1) by Def7

.= o by A39, A38, A4, Def6 ;

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 = (multR (x,o)) . (ab,c1) by Def8

.= multR (ab,c1) by Def7

.= o by A39, A35, A38, Def6

.= multR (a1,bc) by A40, A34, A3, Def6

.= (multR (x,o)) . (a1,(b * c)) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A41:
the multF of F . (x,c1) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A42: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= x * cR by A41, A38, A4, Def6 ;

then b * c <> o by 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;

A43: (a * b) * c = (multR (x,o)) . (ab,c1) by Def8

.= multR (ab,c1) by Def7

.= the multF of F . (x,c1) by A35, A38, A41, Def6 ;

(a * b) * c = (multR (x,o)) . (ab,c1) by Def8

.= multR (ab,c1) by Def7

.= (x * x) * cR by A34, A35, A38, A41, Def6

.= x * (x * cR) by GROUP_1:def 3

.= the multF of F . (x,bc) by A42 ;

hence (a * b) * c = multR (a1,bc) by A41, A43, A42, A1, A3, Def6

.= (multR (x,o)) . (a1,(b * c)) by Def7

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

:: thesis: verum

end;.= multR (b1,c1) by Def7

.= x * cR by A41, A38, A4, Def6 ;

then b * c <> o by 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;

A43: (a * b) * c = (multR (x,o)) . (ab,c1) by Def8

.= multR (ab,c1) by Def7

.= the multF of F . (x,c1) by A35, A38, A41, Def6 ;

(a * b) * c = (multR (x,o)) . (ab,c1) by Def8

.= multR (ab,c1) by Def7

.= (x * x) * cR by A34, A35, A38, A41, Def6

.= x * (x * cR) by GROUP_1:def 3

.= the multF of F . (x,bc) by A42 ;

hence (a * b) * c = multR (a1,bc) by A41, A43, A42, A1, A3, Def6

.= (multR (x,o)) . (a1,(b * c)) by Def7

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

:: thesis: verum

suppose A44:
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;

A45: the multF of F . (x,b) = x * bR

.= bR * x by GROUP_1:def 12

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

A45: the multF of F . (x,b) = x * bR

.= bR * x by GROUP_1:def 12

.= the multF of F . (b,x) ;

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

end;

suppose A46:
the multF of F . (x,b) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A47: a * b =
(multR (x,o)) . (a1,b1)
by Def8

.= multR (a1,b1) by Def7

.= x * bR by A46, A44, A3, Def6 ;

then A48: 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;.= multR (a1,b1) by Def7

.= x * bR by A46, A44, A3, Def6 ;

then A48: 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 A49:
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;

A50: b * c = (multR (x,o)) . (b1,c1) by Def8

.= multR (b1,c1) by Def7

.= bR * x by A45, A46, A49, A44, Def6 ;

then A51: b * c <> o by 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;

A52: the multF of F . (ab,x) = (x * bR) * x by A47

.= x * (bR * x) by GROUP_1:def 3 ;

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

A50: b * c = (multR (x,o)) . (b1,c1) by Def8

.= multR (b1,c1) by Def7

.= bR * x by A45, A46, A49, A44, Def6 ;

then A51: b * c <> o by 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;

A52: the multF of F . (ab,x) = (x * bR) * x by A47

.= x * (bR * x) by GROUP_1:def 3 ;

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

end;

suppose A53:
the multF of F . (ab,x) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= the multF of F . (ab,x) by A47, A1, Def6, A49, A53

.= multR (a1,bc) by A53, A52, A50, A1, A3, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= the multF of F . (ab,x) by A47, A1, Def6, A49, A53

.= multR (a1,bc) by A53, A52, A50, A1, A3, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A54:
the multF of F . (ab,x) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= o by A48, A49, A54, Def6

.= multR (a1,bc) by A54, A52, A50, A51, A3, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= o by A48, A49, A54, Def6

.= multR (a1,bc) by A54, A52, A50, A51, A3, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A55:
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;

A56: the multF of F . (ab,c) = (x * bR) * cR by A47

.= x * (bR * cR) by GROUP_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;

A56: the multF of F . (ab,c) = (x * bR) * cR by A47

.= x * (bR * cR) by GROUP_1:def 3 ;

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

end;

suppose A57:
the multF of F . (b,c) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A58: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= bR * cR by A57, A55, A44, Def6 ;

then A59: b * c <> o by 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;

end;.= multR (b1,c1) by Def7

.= bR * cR by A57, A55, A44, Def6 ;

then A59: b * c <> o by 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;

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

end;

suppose A60:
the multF of F . (ab,c1) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= (x * bR) * cR by A47, A60, A55, A48, Def6

.= x * (bR * cR) by GROUP_1:def 3

.= multR (a1,bc) by A3, A56, A60, A58, A1, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= (x * bR) * cR by A47, A60, A55, A48, Def6

.= x * (bR * cR) by GROUP_1:def 3

.= multR (a1,bc) by A3, A56, A60, A58, A1, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A61:
the multF of F . (ab,c1) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= o by A61, A55, A48, Def6

.= multR (a1,bc) by A3, A56, A61, A58, A59, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= o by A61, A55, A48, Def6

.= multR (a1,bc) by A3, A56, A61, A58, A59, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A62:
the multF of F . (b,c) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A63: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= o by A62, A55, A44, Def6 ;

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;.= multR (b1,c1) by Def7

.= o by A62, A55, A44, Def6 ;

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 multF of F . (ab,c1) <> x or the multF of F . (ab,c1) = x )
;

end;

suppose A64:
the multF of F . (ab,c1) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= (x * bR) * cR by A47, A64, A55, A48, Def6

.= x * (bR * cR) by GROUP_1:def 3

.= multR (a1,bc) by A62, A3, A56, A64, A63, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= (x * bR) * cR by A47, A64, A55, A48, Def6

.= x * (bR * cR) by GROUP_1:def 3

.= multR (a1,bc) by A62, A3, A56, A64, A63, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A65:
the multF of F . (ab,c1) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= o by A65, A55, A48, Def6

.= multR (a1,bc) by A62, A3, A56, A65, A63, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= o by A65, A55, A48, Def6

.= multR (a1,bc) by A62, A3, A56, A65, A63, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A66:
the multF of F . (x,b) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A67:
x <> 0. F
by Def2;

A68: x = x * bR by A66

.= bR * x by GROUP_1:def 12 ;

A69: bR = bR * (1_ F)

.= bR * (x * (x ")) by A67, VECTSP_2:9

.= x * (x ") by A68, GROUP_1:def 3

.= 1_ F by A67, VECTSP_2:9 ;

A70: a * b = (multR (x,o)) . (a1,b1) by Def8

.= multR (a1,b1) by Def7

.= o by A66, A44, A3, Def6 ;

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;A68: x = x * bR by A66

.= bR * x by GROUP_1:def 12 ;

A69: bR = bR * (1_ F)

.= bR * (x * (x ")) by A67, VECTSP_2:9

.= x * (x ") by A68, GROUP_1:def 3

.= 1_ F by A67, VECTSP_2:9 ;

A70: a * b = (multR (x,o)) . (a1,b1) by Def8

.= multR (a1,b1) by Def7

.= o by A66, A44, A3, Def6 ;

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

A72: b * c = (multR (x,o)) . (b1,c1) by Def8

.= multR (b1,c1) by Def7

.= o by A45, A66, A71, A44, Def6 ;

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 = a * (b * c) by A70, A71, A72, A3; :: thesis: verum

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

A72: b * c = (multR (x,o)) . (b1,c1) by Def8

.= multR (b1,c1) by Def7

.= o by A45, A66, A71, A44, Def6 ;

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 = a * (b * c) by A70, A71, A72, A3; :: thesis: verum

suppose A73:
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 A74: 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;

A75: bR <> 0. F by A69;

.= multR (b1,c1) by Def7

.= bR * cR by A76, A73, A44, Def6 ;

then A79: b * c <> o by 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;

A80: x * (bR * cR) = (x * bR) * cR by GROUP_1:def 3

.= x * cR by A66 ;

end;then A74: 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;

A75: bR <> 0. F by A69;

A76: now :: thesis: not the multF of F . (b,c) = x

A78: b * c =
(multR (x,o)) . (b1,c1)
by Def8
assume
the multF of F . (b,c) = x
; :: thesis: contradiction

then bR * cR = x * bR by A66

.= bR * x by GROUP_1:def 12 ;

then cR = x by A75, ALGSTR_0:def 36, ALGSTR_0:def 20;

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

hence contradiction by A74, XBOOLE_0:def 5; :: thesis: verum

end;then bR * cR = x * bR by A66

.= bR * x by GROUP_1:def 12 ;

then cR = x by A75, ALGSTR_0:def 36, ALGSTR_0:def 20;

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

hence contradiction by A74, XBOOLE_0:def 5; :: thesis: verum

.= multR (b1,c1) by Def7

.= bR * cR by A76, A73, A44, Def6 ;

then A79: b * c <> o by 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;

A80: x * (bR * cR) = (x * bR) * cR by GROUP_1:def 3

.= x * cR by A66 ;

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

end;

suppose A81:
the multF of F . (x,c1) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= the multF of F . (x,c1) by A70, A81, A73, Def6

.= multR (a1,bc) by A80, A3, A81, A78, A1, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= the multF of F . (x,c1) by A70, A81, A73, Def6

.= multR (a1,bc) by A80, A3, A81, A78, A1, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

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

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= o by A82, A73, A70, Def6

.= multR (a1,bc) by A79, A82, A80, A3, A78, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= o by A82, A73, A70, Def6

.= multR (a1,bc) by A79, A82, A80, A3, A78, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

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

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

then A84: 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 A84: 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 A85:
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 multF of F . (a1,x) = x or the multF of F . (a1,x) <> x )
;

end;

suppose A86:
the multF of F . (a1,x) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A87:
x <> 0. F
by Def2;

aR = aR * (1_ F)

.= aR * (x * (x ")) by A87, VECTSP_2:9

.= (aR * x) * (x ") by GROUP_1:def 3

.= 1_ F by A86, A87, VECTSP_2:9 ;

then A88: aR <> 0. F ;

A89: a * b = (multR (x,o)) . (a1,b1) by Def8

.= multR (a1,b1) by Def7

.= o by A86, A85, A83, Def6 ;

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;aR = aR * (1_ F)

.= aR * (x * (x ")) by A87, VECTSP_2:9

.= (aR * x) * (x ") by GROUP_1:def 3

.= 1_ F by A86, A87, VECTSP_2:9 ;

then A88: aR <> 0. F ;

A89: a * b = (multR (x,o)) . (a1,b1) by Def8

.= multR (a1,b1) by Def7

.= o by A86, A85, A83, Def6 ;

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 A90:
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 multF of F . (x,x) = x or the multF of F . (x,x) <> x )
;

end;

suppose A91:
the multF of F . (x,x) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A92: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= o by A90, A85, A91, Def6 ;

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 = (multR (x,o)) . (ab,c1) by Def8

.= multR (ab,c1) by Def7

.= o by A89, A90, A91, Def6

.= multR (a1,bc) by A86, A83, A92, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (b1,c1) by Def7

.= o by A90, A85, A91, Def6 ;

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 = (multR (x,o)) . (ab,c1) by Def8

.= multR (ab,c1) by Def7

.= o by A89, A90, A91, Def6

.= multR (a1,bc) by A86, A83, A92, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A93:
the multF of F . (x,x) <> x
; :: thesis: b_{1} * (b_{2} * b_{3}) = (b_{1} * b_{2}) * b_{3}

A94: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= x * x by A93, A90, A85, Def6 ;

then A95: b * c <> o by A1;

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

then A96: 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;

A97: (a * b) * c = (multR (x,o)) . (ab,c1) by Def8

.= multR (ab,c1) by Def7

.= (aR * x) * x by A86, A89, A90, A93, Def6 ;

.= (multR (x,o)) . (a,bc) by Def7

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

hence a * (b * c) = aR * (x * x) by A94

.= (a * b) * c by A97, GROUP_1:def 3 ;

:: thesis: verum

end;.= multR (b1,c1) by Def7

.= x * x by A93, A90, A85, Def6 ;

then A95: b * c <> o by A1;

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

then A96: 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;

A97: (a * b) * c = (multR (x,o)) . (ab,c1) by Def8

.= multR (ab,c1) by Def7

.= (aR * x) * x by A86, A89, A90, A93, Def6 ;

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

then the multF of F . (a1,bc) =
multR (a1,bc)
by A83, A95, Def6
assume
the multF of F . (a1,bc) = x
; :: thesis: contradiction

then aR * bcR = aR * x by A86;

then bcR = x by A88, ALGSTR_0:def 36, ALGSTR_0:def 20;

then b * c in {x} by TARSKI:def 1;

hence contradiction by A96, XBOOLE_0:def 5; :: thesis: verum

end;then aR * bcR = aR * x by A86;

then bcR = x by A88, ALGSTR_0:def 36, ALGSTR_0:def 20;

then b * c in {x} by TARSKI:def 1;

hence contradiction by A96, XBOOLE_0:def 5; :: thesis: verum

.= (multR (x,o)) . (a,bc) by Def7

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

hence a * (b * c) = aR * (x * x) by A94

.= (a * b) * c by A97, GROUP_1:def 3 ;

:: thesis: verum

suppose A99:
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 A100: 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 A100;

end;then A100: 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 A100;

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

end;

suppose A101:
the multF of F . (x,c) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A102: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= o by A101, A99, A85, Def6 ;

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 = (multR (x,o)) . (ab,c1) by Def8

.= multR (ab,c1) by Def7

.= o by A89, A99, A101, Def6

.= multR (a1,bc) by A86, A83, A102, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (b1,c1) by Def7

.= o by A101, A99, A85, Def6 ;

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 = (multR (x,o)) . (ab,c1) by Def8

.= multR (ab,c1) by Def7

.= o by A89, A99, A101, Def6

.= multR (a1,bc) by A86, A83, A102, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A103:
the multF of F . (x,c) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A104: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= x * cR by A103, A99, A85, Def6 ;

then A105: b * c <> o by A1;

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

then A106: 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 A106;

.= multR (ab,c1) by Def7

.= (aR * x) * cR by A86, A89, A99, A103, Def6

.= aR * (x * cR) by GROUP_1:def 3

.= multR (a1,bc) by A107, A105, A83, A104, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (b1,c1) by Def7

.= x * cR by A103, A99, A85, Def6 ;

then A105: b * c <> o by A1;

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

then A106: 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 A106;

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

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8
assume
the multF of F . (a1,bc) = x
; :: thesis: contradiction

then aR * bcR = aR * x by A86;

then bcR = x by A88, ALGSTR_0:def 36, ALGSTR_0:def 20;

then b * c in {x} by TARSKI:def 1;

hence contradiction by A106, XBOOLE_0:def 5; :: thesis: verum

end;then aR * bcR = aR * x by A86;

then bcR = x by A88, ALGSTR_0:def 36, ALGSTR_0:def 20;

then b * c in {x} by TARSKI:def 1;

hence contradiction by A106, XBOOLE_0:def 5; :: thesis: verum

.= multR (ab,c1) by Def7

.= (aR * x) * cR by A86, A89, A99, A103, Def6

.= aR * (x * cR) by GROUP_1:def 3

.= multR (a1,bc) by A107, A105, A83, A104, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

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

A110: a * b =
(multR (x,o)) . (a1,b1)
by Def8

.= multR (a1,b1) by Def7

.= aR * x by A85, A83, A109, Def6 ;

then A111: a * b <> o by A1;

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

then A112: 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 A112;

end;.= multR (a1,b1) by Def7

.= aR * x by A85, A83, A109, Def6 ;

then A111: a * b <> o by A1;

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

then A112: 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 A112;

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

end;

suppose A113:
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 multF of F . (x,x) = x or the multF of F . (x,x) <> x )
;

end;

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

A115: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= o by A114, A113, A85, Def6 ;

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;

.= multR (ab,c1) by Def7

.= (aR * x) * x by A110, A1, A113, A116, Def6

.= aR * (x * x) by GROUP_1:def 3

.= multR (a1,bc) by A114, A109, A83, A115, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (b1,c1) by Def7

.= o by A114, A113, A85, Def6 ;

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;

A116: now :: thesis: not the multF of F . (ab,x) = x

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8
assume
the multF of F . (ab,x) = x
; :: thesis: contradiction

then x = (aR * x) * x by A110

.= aR * (x * x) by GROUP_1:def 3

.= aR * x by A114 ;

hence contradiction by A109; :: thesis: verum

end;then x = (aR * x) * x by A110

.= aR * (x * x) by GROUP_1:def 3

.= aR * x by A114 ;

hence contradiction by A109; :: thesis: verum

.= multR (ab,c1) by Def7

.= (aR * x) * x by A110, A1, A113, A116, Def6

.= aR * (x * x) by GROUP_1:def 3

.= multR (a1,bc) by A114, A109, A83, A115, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A118:
the multF of F . (x,x) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A119: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= x * x by A118, A113, A85, Def6 ;

then A120: b * c <> o by A1;

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

then A121: b * c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;

reconsider bc = b * c as Element of carr (x,o) by Def8;

reconsider bcR = b * c as Element of F by A121;

A122: the multF of F . (a,bc) = aR * (x * x) by A119

.= (aR * x) * x by GROUP_1:def 3

.= the multF of F . (ab,x) by A110 ;

end;.= multR (b1,c1) by Def7

.= x * x by A118, A113, A85, Def6 ;

then A120: b * c <> o by A1;

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

then A121: b * c in ([#] F) \ {x} by A2, XBOOLE_0:def 3;

reconsider bc = b * c as Element of carr (x,o) by Def8;

reconsider bcR = b * c as Element of F by A121;

A122: the multF of F . (a,bc) = aR * (x * x) by A119

.= (aR * x) * x by GROUP_1:def 3

.= the multF of F . (ab,x) by A110 ;

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

end;

suppose A123:
the multF of F . (ab,x) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= o by A111, A113, A123, Def6

.= multR (a1,bc) by A123, A83, A122, A120, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= o by A111, A113, A123, Def6

.= multR (a1,bc) by A123, A83, A122, A120, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A124:
the multF of F . (ab,x) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= the multF of F . (ab,x) by A110, A1, A113, A124, Def6

.= multR (a1,bc) by A124, A83, A122, A120, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= the multF of F . (ab,x) by A110, A1, A113, A124, Def6

.= multR (a1,bc) by A124, A83, A122, A120, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A125:
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 A126: 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 A126;

end;then A126: 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 A126;

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

end;

suppose A127:
the multF of F . (x,c) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A128: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= o by A127, A125, A85, Def6 ;

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;

A129: the multF of F . (ab,c) = (aR * x) * cR by A110

.= aR * (x * cR) by GROUP_1:def 3

.= the multF of F . (a,x) by A127 ;

end;.= multR (b1,c1) by Def7

.= o by A127, A125, A85, Def6 ;

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;

A129: the multF of F . (ab,c) = (aR * x) * cR by A110

.= aR * (x * cR) by GROUP_1:def 3

.= the multF of F . (a,x) by A127 ;

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

end;

suppose A130:
the multF of F . (ab,c1) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= o by A111, A125, A130, Def6

.= multR (a1,bc) by A130, A83, A128, A129, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= o by A111, A125, A130, Def6

.= multR (a1,bc) by A130, A83, A128, A129, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A131:
the multF of F . (ab,c1) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= (aR * x) * cR by A110, A111, A125, A131, Def6

.= aR * (x * cR) by GROUP_1:def 3

.= multR (a1,bc) by A127, A109, A83, A128, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= (aR * x) * cR by A110, A111, A125, A131, Def6

.= aR * (x * cR) by GROUP_1:def 3

.= multR (a1,bc) by A127, A109, A83, A128, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A132:
the multF of F . (x,c) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A133: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= x * cR by A132, A125, A85, Def6 ;

then A134: b * c <> o by A1;

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

then A135: 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 A135;

A136: the multF of F . (a,bc) = aR * (x * cR) by A133

.= (aR * x) * cR by GROUP_1:def 3

.= the multF of F . (ab,c) by A110 ;

end;.= multR (b1,c1) by Def7

.= x * cR by A132, A125, A85, Def6 ;

then A134: b * c <> o by A1;

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

then A135: 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 A135;

A136: the multF of F . (a,bc) = aR * (x * cR) by A133

.= (aR * x) * cR by GROUP_1:def 3

.= the multF of F . (ab,c) by A110 ;

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

end;

suppose A137:
the multF of F . (ab,c1) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= o by A111, A125, A137, Def6

.= multR (a1,bc) by A137, A83, A136, A134, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= o by A111, A125, A137, Def6

.= multR (a1,bc) by A137, A83, A136, A134, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A138:
the multF of F . (ab,c1) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= (aR * x) * cR by A110, A111, A125, A138, Def6

.= aR * (x * cR) by GROUP_1:def 3

.= multR (a1,bc) by A138, A83, A133, A136, A134, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= (aR * x) * cR by A110, A111, A125, A138, Def6

.= aR * (x * cR) by GROUP_1:def 3

.= multR (a1,bc) by A138, A83, A133, A136, A134, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A139:
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 A140: 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 A140;

end;then A140: 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 A140;

A141: now :: thesis: not x = x * x

assume A142:
x = x * x
; :: thesis: contradiction

x <> 0. F by Def2;

then A143: x is left_mult-cancelable by ALGSTR_0:def 36;

x * x = x * (1. F) by A142;

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

end;x <> 0. F by Def2;

then A143: x is left_mult-cancelable by ALGSTR_0:def 36;

x * x = x * (1. F) by A142;

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

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

end;

suppose A144:
the multF of F . (a,b) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A145: a * b =
(multR (x,o)) . (a1,b1)
by Def8

.= multR (a1,b1) by Def7

.= o by A144, A139, A83, Def6 ;

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;.= multR (a1,b1) by Def7

.= o by A144, A139, A83, Def6 ;

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;

A146: now :: thesis: not bR = 0. F

assume
bR = 0. F
; :: thesis: contradiction

then aR * (0. F) = x by A144;

hence contradiction by Def2; :: thesis: verum

end;then aR * (0. F) = x by A144;

hence contradiction by Def2; :: thesis: verum

A148: now :: thesis: not bR * x = x

assume
bR * x = x
; :: thesis: contradiction

then bR * x = aR * bR by A144

.= bR * aR by GROUP_1:def 12 ;

then x = aR by A146, ALGSTR_0:def 36, ALGSTR_0:def 20;

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

hence contradiction by A84, XBOOLE_0:def 5; :: thesis: verum

end;then bR * x = aR * bR by A144

.= bR * aR by GROUP_1:def 12 ;

then x = aR by A146, ALGSTR_0:def 36, ALGSTR_0:def 20;

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

hence contradiction by A84, XBOOLE_0:def 5; :: thesis: verum

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

end;

suppose A150:
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;

A151: b * c = (multR (x,o)) . (b1,c1) by Def8

.= multR (b1,c1) by Def7

.= bR * x by A148, A150, A139, Def6 ;

then A152: b * c <> o by A1;

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

then A153: 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 A153;

.= multR (ab,c1) by Def7

.= (aR * bR) * x by A144, A145, A150, A141, Def6

.= aR * (bR * x) by GROUP_1:def 3

.= multR (a1,bc) by A83, A152, A151, A154, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

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

A151: b * c = (multR (x,o)) . (b1,c1) by Def8

.= multR (b1,c1) by Def7

.= bR * x by A148, A150, A139, Def6 ;

then A152: b * c <> o by A1;

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

then A153: 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 A153;

A154: now :: thesis: not the multF of F . (a,bc) = x

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8
assume
the multF of F . (a,bc) = x
; :: thesis: contradiction

then x = aR * (bR * x) by A151

.= (aR * bR) * x by GROUP_1:def 3

.= x * x by A144 ;

hence contradiction by A141; :: thesis: verum

end;then x = aR * (bR * x) by A151

.= (aR * bR) * x by GROUP_1:def 3

.= x * x by A144 ;

hence contradiction by A141; :: thesis: verum

.= multR (ab,c1) by Def7

.= (aR * bR) * x by A144, A145, A150, A141, Def6

.= aR * (bR * x) by GROUP_1:def 3

.= multR (a1,bc) by A83, A152, A151, A154, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A156:
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 A157: 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 A157;

end;then A157: 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 A157;

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

end;

suppose A158:
the multF of F . (b,c) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A159: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= bR * cR by A156, A139, A158, Def6 ;

then A160: b * c <> o by A1;

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

then A161: 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 A161;

end;.= multR (b1,c1) by Def7

.= bR * cR by A156, A139, A158, Def6 ;

then A160: b * c <> o by A1;

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

then A161: 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 A161;

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

end;

suppose A162:
the multF of F . (x,c) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

.= multR (ab,c1) by Def7

.= (aR * bR) * cR by A144, A145, A156, A162, Def6

.= aR * (bR * cR) by GROUP_1:def 3

.= multR (a1,bc) by A83, A163, A159, A160, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;

A163: now :: thesis: not the multF of F . (a,bc) = x

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8
assume
the multF of F . (a,bc) = x
; :: thesis: contradiction

then x = aR * (bR * cR) by A159

.= (aR * bR) * cR by GROUP_1:def 3

.= x * cR by A144 ;

hence contradiction by A162; :: thesis: verum

end;then x = aR * (bR * cR) by A159

.= (aR * bR) * cR by GROUP_1:def 3

.= x * cR by A144 ;

hence contradiction by A162; :: thesis: verum

.= multR (ab,c1) by Def7

.= (aR * bR) * cR by A144, A145, A156, A162, Def6

.= aR * (bR * cR) by GROUP_1:def 3

.= multR (a1,bc) by A83, A163, A159, A160, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A164:
the multF of F . (x,c) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A165: aR * (bR * cR) =
(aR * bR) * cR
by GROUP_1:def 3

.= x by A144, A164 ;

thus (a * b) * c = (multR (x,o)) . (ab,c1) by Def8

.= multR (ab,c1) by Def7

.= o by A164, A145, A156, Def6

.= multR (a1,bc) by A165, A83, A160, A159, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= x by A144, A164 ;

thus (a * b) * c = (multR (x,o)) . (ab,c1) by Def8

.= multR (ab,c1) by Def7

.= o by A164, A145, A156, Def6

.= multR (a1,bc) by A165, A83, A160, A159, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A166:
the multF of F . (b,c) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

then bR * cR =
aR * bR
by A144

.= bR * aR by GROUP_1:def 12 ;

then A167: cR = aR by A146, ALGSTR_0:def 36, ALGSTR_0:def 20;

A168: b * c = (multR (x,o)) . (b1,c1) by Def8

.= multR (b1,c1) by Def7

.= o by A156, A139, A166, Def6 ;

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;

A169: x * cR = aR * x by A167, GROUP_1:def 12

.= the multF of F . (a,x) ;

end;.= bR * aR by GROUP_1:def 12 ;

then A167: cR = aR by A146, ALGSTR_0:def 36, ALGSTR_0:def 20;

A168: b * c = (multR (x,o)) . (b1,c1) by Def8

.= multR (b1,c1) by Def7

.= o by A156, A139, A166, Def6 ;

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;

A169: x * cR = aR * x by A167, GROUP_1:def 12

.= the multF of F . (a,x) ;

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

end;

suppose A170:
the multF of F . (x,c) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= x * cR by A145, A156, A170, Def6

.= multR (a1,bc) by A83, A169, A170, A168, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= x * cR by A145, A156, A170, Def6

.= multR (a1,bc) by A83, A169, A170, A168, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A171:
the multF of F . (x,c) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= o by A145, A156, A171, Def6

.= multR (a1,bc) by A83, A169, A171, A168, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= o by A145, A156, A171, Def6

.= multR (a1,bc) by A83, A169, A171, A168, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A172:
the multF of F . (a,b) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A173: a * b =
(multR (x,o)) . (a1,b1)
by Def8

.= multR (a1,b1) by Def7

.= aR * bR by A172, A139, A83, Def6 ;

then A174: a * b <> o by A1;

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

then A175: 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 A175;

end;.= multR (a1,b1) by Def7

.= aR * bR by A172, A139, A83, Def6 ;

then A174: a * b <> o by A1;

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

then A175: 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 A175;

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

end;

suppose A176:
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 multF of F . (b,x) <> x or the multF of F . (b,x) = x )
;

end;

suppose A177:
the multF of F . (b,x) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A178: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= bR * x by A176, A139, A177, Def6 ;

then A179: b * c <> o by A1;

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

then A180: 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 A180;

A181: the multF of F . (ab,x) = (aR * bR) * x by A173

.= aR * (bR * x) by GROUP_1:def 3

.= the multF of F . (a,bc) by A178 ;

end;.= multR (b1,c1) by Def7

.= bR * x by A176, A139, A177, Def6 ;

then A179: b * c <> o by A1;

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

then A180: 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 A180;

A181: the multF of F . (ab,x) = (aR * bR) * x by A173

.= aR * (bR * x) by GROUP_1:def 3

.= the multF of F . (a,bc) by A178 ;

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

end;

suppose A182:
the multF of F . (ab,x) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= (aR * bR) * x by A173, A1, A176, A182, Def6

.= aR * (bR * x) by GROUP_1:def 3

.= multR (a1,bc) by A83, A182, A181, A178, A179, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= (aR * bR) * x by A173, A1, A176, A182, Def6

.= aR * (bR * x) by GROUP_1:def 3

.= multR (a1,bc) by A83, A182, A181, A178, A179, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A183:
the multF of F . (ab,x) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= o by A174, A176, A183, Def6

.= multR (a1,bc) by A83, A183, A181, A179, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= o by A174, A176, A183, Def6

.= multR (a1,bc) by A83, A183, A181, A179, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A184:
the multF of F . (b,x) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A185: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= o by A176, A139, A184, Def6 ;

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;

A186: (aR * bR) * x = aR * (bR * x) by GROUP_1:def 3

.= the multF of F . (a,x) by A184 ;

end;.= multR (b1,c1) by Def7

.= o by A176, A139, A184, Def6 ;

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;

A186: (aR * bR) * x = aR * (bR * x) by GROUP_1:def 3

.= the multF of F . (a,x) by A184 ;

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

end;

suppose A187:
the multF of F . (ab,x) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= (aR * bR) * x by A173, A1, A176, A187, Def6

.= multR (a1,bc) by A173, A83, A187, A185, A186, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= (aR * bR) * x by A173, A1, A176, A187, Def6

.= multR (a1,bc) by A173, A83, A187, A185, A186, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A188:
the multF of F . (ab,x) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= o by A174, A176, A188, Def6

.= multR (a1,bc) by A173, A83, A188, A185, A186, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= o by A174, A176, A188, Def6

.= multR (a1,bc) by A173, A83, A188, A185, A186, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A189:
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 A190: 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 A190;

end;then A190: 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 A190;

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

end;

suppose A191:
the multF of F . (b,c) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A192: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= bR * cR by A189, A139, A191, Def6 ;

then A193: b * c <> o by A1;

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

then A194: 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 A194;

A195: the multF of F . (ab,c) = (aR * bR) * cR by A173

.= aR * (bR * cR) by GROUP_1:def 3

.= the multF of F . (a,bc) by A192 ;

end;.= multR (b1,c1) by Def7

.= bR * cR by A189, A139, A191, Def6 ;

then A193: b * c <> o by A1;

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

then A194: 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 A194;

A195: the multF of F . (ab,c) = (aR * bR) * cR by A173

.= aR * (bR * cR) by GROUP_1:def 3

.= the multF of F . (a,bc) by A192 ;

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

end;

suppose A196:
the multF of F . (ab,c) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= (aR * bR) * cR by A173, A174, A189, A196, Def6

.= aR * (bR * cR) by GROUP_1:def 3

.= multR (a1,bc) by A193, A83, A196, A192, A195, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= (aR * bR) * cR by A173, A174, A189, A196, Def6

.= aR * (bR * cR) by GROUP_1:def 3

.= multR (a1,bc) by A193, A83, A196, A192, A195, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A197:
the multF of F . (ab,c) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= o by A174, A189, A197, Def6

.= multR (a1,bc) by A193, A83, A197, A195, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= o by A174, A189, A197, Def6

.= multR (a1,bc) by A193, A83, A197, A195, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A198:
the multF of F . (b,c) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

A199: b * c =
(multR (x,o)) . (b1,c1)
by Def8

.= multR (b1,c1) by Def7

.= o by A189, A139, A198, Def6 ;

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;

A200: (aR * bR) * cR = aR * (bR * cR) by GROUP_1:def 3

.= the multF of F . (a,x) by A198 ;

end;.= multR (b1,c1) by Def7

.= o by A189, A139, A198, Def6 ;

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;

A200: (aR * bR) * cR = aR * (bR * cR) by GROUP_1:def 3

.= the multF of F . (a,x) by A198 ;

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

end;

suppose A201:
the multF of F . (ab,c) <> x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= (aR * bR) * cR by A173, A174, A189, A201, Def6

.= multR (a1,bc) by A173, A83, A201, A199, A200, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= (aR * bR) * cR by A173, A174, A189, A201, Def6

.= multR (a1,bc) by A173, A83, A201, A199, A200, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

suppose A202:
the multF of F . (ab,c) = x
; :: thesis: (b_{1} * b_{2}) * b_{3} = b_{1} * (b_{2} * b_{3})

thus (a * b) * c =
(multR (x,o)) . (ab,c1)
by Def8

.= multR (ab,c1) by Def7

.= o by A174, A189, A202, Def6

.= multR (a1,bc) by A173, A83, A202, A199, A200, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum

end;.= multR (ab,c1) by Def7

.= o by A174, A189, A202, Def6

.= multR (a1,bc) by A173, A83, A202, A199, A200, Def6

.= (multR (x,o)) . (a,bc) by Def7

.= a * (b * c) by Def8 ; :: thesis: verum