set R = F;

A1: [#] (ExField (x,o)) = carr (x,o) by Def8;

A1: [#] (ExField (x,o)) = carr (x,o) by Def8;

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

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

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

end;

suppose A2:
b = o
; :: thesis: b_{1} + b_{2} = b_{2} + b_{1}

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
( a = o or a <> o )
;

end;

suppose A3:
a = o
; :: thesis: b_{1} + b_{2} = b_{2} + b_{1}

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

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

thus a + b = b + a by A2, A3; :: thesis: verum

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

thus a + b = b + a by A2, A3; :: thesis: verum

suppose A4:
a <> o
; :: thesis: b_{1} + b_{2} = b_{2} + b_{1}

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

then A5: a in ([#] F) \ {x} by A1, XBOOLE_0:def 3;

reconsider a1 = a as Element of carr (x,o) by Def8;

reconsider aR = a as Element of F by A5;

A6: the addF of F . (a1,x) = aR + x

.= x + aR

.= the addF of F . (x,a1) ;

end;then A5: a in ([#] F) \ {x} by A1, XBOOLE_0:def 3;

reconsider a1 = a as Element of carr (x,o) by Def8;

reconsider aR = a as Element of F by A5;

A6: the addF of F . (a1,x) = aR + x

.= x + aR

.= the addF of F . (x,a1) ;

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

end;

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

thus a + b =
(addR (x,o)) . (a1,b1)
by Def8

.= addR (a1,b1) by Def5

.= the addF of F . (a,x) by A7, A4, A2, Def4

.= addR (b1,a1) by A2, A4, A6, A7, Def4

.= (addR (x,o)) . (b1,a1) by Def5

.= b + a by Def8 ; :: thesis: verum

end;.= addR (a1,b1) by Def5

.= the addF of F . (a,x) by A7, A4, A2, Def4

.= addR (b1,a1) by A2, A4, A6, A7, Def4

.= (addR (x,o)) . (b1,a1) by Def5

.= b + a by Def8 ; :: thesis: verum

suppose A9:
b <> o
; :: thesis: b_{1} + b_{2} = b_{2} + b_{1}

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

then A10: b in ([#] F) \ {x} by A1, XBOOLE_0:def 3;

reconsider b1 = b as Element of carr (x,o) by Def8;

end;then A10: b in ([#] F) \ {x} by A1, XBOOLE_0:def 3;

reconsider b1 = b as Element of carr (x,o) by Def8;

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

end;

suppose A11:
a = o
; :: thesis: b_{1} + b_{2} = b_{2} + b_{1}

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

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

reconsider bR = b as Element of F by A10;

A12: the addF of F . (x,b1) = x + bR

.= bR + x

.= the addF of F . (b1,x) ;

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

reconsider bR = b as Element of F by A10;

A12: the addF of F . (x,b1) = x + bR

.= bR + x

.= the addF of F . (b1,x) ;

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

end;

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

thus a + b =
(addR (x,o)) . (a1,b1)
by Def8

.= addR (a1,b1) by Def5

.= the addF of F . (x,b) by A13, A11, A9, Def4

.= addR (b1,a1) by A9, A11, A12, A13, Def4

.= (addR (x,o)) . (b1,a1) by Def5

.= b + a by Def8 ; :: thesis: verum

end;.= addR (a1,b1) by Def5

.= the addF of F . (x,b) by A13, A11, A9, Def4

.= addR (b1,a1) by A9, A11, A12, A13, Def4

.= (addR (x,o)) . (b1,a1) by Def5

.= b + a by Def8 ; :: thesis: verum

suppose A15:
a <> o
; :: thesis: b_{1} + b_{2} = b_{2} + b_{1}

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

then A16: a in ([#] F) \ {x} by A1, XBOOLE_0:def 3;

reconsider a1 = a as Element of carr (x,o) by Def8;

reconsider aR = a, bR = b as Element of [#] F by A10, A16;

A17: the addF of F . (a,b) = aR + bR

.= bR + aR

.= the addF of F . (b,a) ;

end;then A16: a in ([#] F) \ {x} by A1, XBOOLE_0:def 3;

reconsider a1 = a as Element of carr (x,o) by Def8;

reconsider aR = a, bR = b as Element of [#] F by A10, A16;

A17: the addF of F . (a,b) = aR + bR

.= bR + aR

.= the addF of F . (b,a) ;

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

end;

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

thus a + b =
(addR (x,o)) . (a1,b1)
by Def8

.= addR (a1,b1) by Def5

.= the addF of F . (a,b) by A9, A15, A18, Def4

.= addR (b1,a1) by A9, A15, A17, A18, Def4

.= (addR (x,o)) . (b1,a1) by Def5

.= b + a by Def8 ; :: thesis: verum

end;.= addR (a1,b1) by Def5

.= the addF of F . (a,b) by A9, A15, A18, Def4

.= addR (b1,a1) by A9, A15, A17, A18, Def4

.= (addR (x,o)) . (b1,a1) by Def5

.= b + a by Def8 ; :: thesis: verum