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 right_zeroed & ExField (x,o) is right_complementable )

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

( ExField (x,o) is right_zeroed & ExField (x,o) is right_complementable )

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

assume a1: not o in [#] F ; :: thesis: ( ExField (x,o) is right_zeroed & ExField (x,o) is right_complementable )

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

set C = carr (x,o);

set ADDR = the addF of F;

consider xi being Element of F such that

A2: x + xi = 0. F by ALGSTR_0:def 11;

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

o in {o} by TARSKI:def 1;

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

reconsider u = u1 as Element of (ExField (x,o)) by Def8;

for o being object st not o in [#] F holds

( ExField (x,o) is right_zeroed & ExField (x,o) is right_complementable )

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

( ExField (x,o) is right_zeroed & ExField (x,o) is right_complementable )

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

assume a1: not o in [#] F ; :: thesis: ( ExField (x,o) is right_zeroed & ExField (x,o) is right_complementable )

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

set C = carr (x,o);

set ADDR = the addF of F;

consider xi being Element of F such that

A2: x + xi = 0. F by ALGSTR_0:def 11;

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

o in {o} by TARSKI:def 1;

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

reconsider u = u1 as Element of (ExField (x,o)) by Def8;

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

hence
ExField (x,o) is right_zeroed
by RLVECT_1:def 4; :: thesis: ExField (x,o) is right_complementable let a be Element of (ExField (x,o)); :: thesis: b_{1} + (0. (ExField (x,o))) = b_{1}

A4: 0. (ExField (x,o)) = 0. F by Def8;

0. F <> x by Def2;

then not 0. F in {x} by TARSKI:def 1;

then 0. F in ([#] F) \ {x} by XBOOLE_0:def 5;

then reconsider u = 0. F as Element of carr (x,o) by XBOOLE_0:def 3;

A5: o <> u by a1;

end;A4: 0. (ExField (x,o)) = 0. F by Def8;

0. F <> x by Def2;

then not 0. F in {x} by TARSKI:def 1;

then 0. F in ([#] F) \ {x} by XBOOLE_0:def 5;

then reconsider u = 0. F as Element of carr (x,o) by XBOOLE_0:def 3;

A5: o <> u by a1;

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

end;

suppose A6:
a = o
; :: thesis: b_{1} + (0. (ExField (x,o))) = 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;

A7: the addF of F . (x,(0. F)) = x + (0. F)

.= x ;

thus a + (0. (ExField (x,o))) = (addR (x,o)) . (a1,u) by A4, Def8

.= addR (a1,u) by Def5

.= a by A5, A6, A7, Def4 ; :: thesis: verum

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

A7: the addF of F . (x,(0. F)) = x + (0. F)

.= x ;

thus a + (0. (ExField (x,o))) = (addR (x,o)) . (a1,u) by A4, Def8

.= addR (a1,u) by Def5

.= a by A5, A6, A7, Def4 ; :: thesis: verum

suppose A8:
a <> o
; :: thesis: b_{1} + (0. (ExField (x,o))) = b_{1}

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

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

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

reconsider aR = a as Element of [#] F by A9;

A10: the addF of F . (a,u) = aR + (0. F)

.= aR ;

not aR in {x} by A9, XBOOLE_0:def 5;

then A11: the addF of F . (a,u) <> x by A10, TARSKI:def 1;

thus a + (0. (ExField (x,o))) = (addR (x,o)) . (a1,u) by A4, Def8

.= addR (a1,u) by Def5

.= aR + (0. F) by A8, A5, A11, Def4

.= a ; :: thesis: verum

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

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

reconsider aR = a as Element of [#] F by A9;

A10: the addF of F . (a,u) = aR + (0. F)

.= aR ;

not aR in {x} by A9, XBOOLE_0:def 5;

then A11: the addF of F . (a,u) <> x by A10, TARSKI:def 1;

thus a + (0. (ExField (x,o))) = (addR (x,o)) . (a1,u) by A4, Def8

.= addR (a1,u) by Def5

.= aR + (0. F) by A8, A5, A11, Def4

.= a ; :: thesis: verum

now :: thesis: for a being Element of (ExField (x,o)) holds a is right_complementable

hence
ExField (x,o) is right_complementable
by ALGSTR_0:def 16; :: thesis: verumlet a be Element of (ExField (x,o)); :: thesis: b_{1} is right_complementable

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

end;

suppose A12:
a = o
; :: thesis: b_{1} is right_complementable

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
( xi = x or xi <> x )
;

end;

suppose A13:
xi = x
; :: thesis: b_{1} is right_complementable

then A14:
the addF of F . (x,x) <> x
by A2, Def2;

a + u = (addR (x,o)) . (a1,u1) by Def8

.= addR (a1,u1) by Def5

.= the addF of F . (x,xi) by A12, A13, A14, Def4

.= 0. (ExField (x,o)) by A2, Def8 ;

hence a is right_complementable by ALGSTR_0:def 11; :: thesis: verum

end;a + u = (addR (x,o)) . (a1,u1) by Def8

.= addR (a1,u1) by Def5

.= the addF of F . (x,xi) by A12, A13, A14, Def4

.= 0. (ExField (x,o)) by A2, Def8 ;

hence a is right_complementable by ALGSTR_0:def 11; :: thesis: verum

suppose
xi <> x
; :: thesis: b_{1} is right_complementable

then
not xi in {x}
by TARSKI:def 1;

then xi in ([#] F) \ {x} by XBOOLE_0:def 5;

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

reconsider b = x1i as Element of (ExField (x,o)) by Def8;

A15: the addF of F . (x,b) <> x by A2, Def2;

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

.= addR (a1,x1i) by Def5

.= the addF of F . (x,xi) by A1, A12, A15, Def4

.= 0. (ExField (x,o)) by A2, Def8 ;

hence a is right_complementable by ALGSTR_0:def 11; :: thesis: verum

end;then xi in ([#] F) \ {x} by XBOOLE_0:def 5;

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

reconsider b = x1i as Element of (ExField (x,o)) by Def8;

A15: the addF of F . (x,b) <> x by A2, Def2;

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

.= addR (a1,x1i) by Def5

.= the addF of F . (x,xi) by A1, A12, A15, Def4

.= 0. (ExField (x,o)) by A2, Def8 ;

hence a is right_complementable by ALGSTR_0:def 11; :: thesis: verum

suppose A16:
a <> o
; :: thesis: b_{1} is right_complementable

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

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

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

reconsider aR = a as Element of [#] F by A17;

consider aRi being Element of F such that

A18: aR + aRi = 0. F by ALGSTR_0:def 11;

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

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

reconsider aR = a as Element of [#] F by A17;

consider aRi being Element of F such that

A18: aR + aRi = 0. F by ALGSTR_0:def 11;

per cases
( aRi = x or aRi <> x )
;

end;

suppose A19:
aRi = x
; :: thesis: b_{1} is right_complementable

then A20:
the addF of F . (a,x) <> x
by A18, Def2;

a + u = (addR (x,o)) . (a1,u1) by Def8

.= addR (a1,u1) by Def5

.= the addF of F . (aR,aRi) by A16, A19, A20, Def4

.= 0. (ExField (x,o)) by A18, Def8 ;

hence a is right_complementable by ALGSTR_0:def 11; :: thesis: verum

end;a + u = (addR (x,o)) . (a1,u1) by Def8

.= addR (a1,u1) by Def5

.= the addF of F . (aR,aRi) by A16, A19, A20, Def4

.= 0. (ExField (x,o)) by A18, Def8 ;

hence a is right_complementable by ALGSTR_0:def 11; :: thesis: verum

suppose
aRi <> x
; :: thesis: b_{1} is right_complementable

then
not aRi in {x}
by TARSKI:def 1;

then aRi in ([#] F) \ {x} by XBOOLE_0:def 5;

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

reconsider b = a1i as Element of (ExField (x,o)) by Def8;

A21: the addF of F . (a,b) <> x by A18, Def2;

A22: ( aR <> o & aRi <> o ) by a1;

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

.= addR (a1,a1i) by Def5

.= the addF of F . (aR,aRi) by A21, A22, Def4

.= 0. (ExField (x,o)) by A18, Def8 ;

hence a is right_complementable by ALGSTR_0:def 11; :: thesis: verum

end;then aRi in ([#] F) \ {x} by XBOOLE_0:def 5;

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

reconsider b = a1i as Element of (ExField (x,o)) by Def8;

A21: the addF of F . (a,b) <> x by A18, Def2;

A22: ( aR <> o & aRi <> o ) by a1;

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

.= addR (a1,a1i) by Def5

.= the addF of F . (aR,aRi) by A21, A22, Def4

.= 0. (ExField (x,o)) by A18, Def8 ;

hence a is right_complementable by ALGSTR_0:def 11; :: thesis: verum