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;
now :: thesis: for a being Element of (ExField (x,o)) holds a + (0. (ExField (x,o))) = a
let a be Element of (ExField (x,o)); :: thesis: b1 + (0. (ExField (x,o))) = b1
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 ) ;
suppose A6: a = o ; :: thesis: b1 + (0. (ExField (x,o))) = b1
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
.= addR (a1,u) by Def5
.= a by A5, A6, A7, Def4 ; :: thesis: verum
end;
suppose A8: a <> o ; :: thesis: b1 + (0. (ExField (x,o))) = b1
then not a in {o} by TARSKI:def 1;
then A9: a in ([#] F) \ {x} by ;
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 ;
then A11: the addF of F . (a,u) <> x by ;
thus a + (0. (ExField (x,o))) = (addR (x,o)) . (a1,u) by
.= addR (a1,u) by Def5
.= aR + (0. F) by A8, A5, A11, Def4
.= a ; :: thesis: verum
end;
end;
end;
hence ExField (x,o) is right_zeroed by RLVECT_1:def 4; :: thesis: ExField (x,o) is right_complementable
now :: thesis: for a being Element of (ExField (x,o)) holds a is right_complementable
let a be Element of (ExField (x,o)); :: thesis:
per cases ( a = o or a <> o ) ;
suppose A12: a = o ; :: thesis:
then a in {o} by TARSKI:def 1;
then reconsider a1 = a as Element of carr (x,o) by XBOOLE_0:def 3;
per cases ( xi = x or xi <> x ) ;
suppose A13: xi = x ; :: thesis:
then A14: the addF of F . (x,x) <> x by ;
a + u = (addR (x,o)) . (a1,u1) by Def8
.= addR (a1,u1) by Def5
.= the addF of F . (x,xi) by
.= 0. (ExField (x,o)) by ;
hence a is right_complementable by ALGSTR_0:def 11; :: thesis: verum
end;
suppose xi <> x ; :: thesis:
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 ;
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 ;
hence a is right_complementable by ALGSTR_0:def 11; :: thesis: verum
end;
end;
end;
suppose A16: a <> o ; :: thesis:
then not a in {o} by TARSKI:def 1;
then A17: a in ([#] F) \ {x} by ;
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 ) ;
suppose A19: aRi = x ; :: thesis:
then A20: the addF of F . (a,x) <> x by ;
a + u = (addR (x,o)) . (a1,u1) by Def8
.= addR (a1,u1) by Def5
.= the addF of F . (aR,aRi) by
.= 0. (ExField (x,o)) by ;
hence a is right_complementable by ALGSTR_0:def 11; :: thesis: verum
end;
suppose aRi <> x ; :: thesis:
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 ;
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
.= 0. (ExField (x,o)) by ;
hence a is right_complementable by ALGSTR_0:def 11; :: thesis: verum
end;
end;
end;
end;
end;
hence ExField (x,o) is right_complementable by ALGSTR_0:def 16; :: thesis: verum