set K = RenField r;
thus RenField r is Abelian :: thesis: ( RenField r is add-associative & RenField r is right_zeroed & RenField r is right_complementable )

proof

now :: thesis: for a, b being Element of (RenField r) holds a + b = b + a

let a, b be Element of (RenField r); :: thesis: a + b = b + a
reconsider a1 = a, b1 = b as Element of rng r by defrf;
thus a + b = (ren_add r) . (a,b) by defrf
.= r . (((r ") . a1) + ((r ") . b1)) by defra
.= (ren_add r) . (b,a) by defra
.= b + a by defrf ; :: thesis: verum

end;

hence RenField r is Abelian ; :: thesis: verum

end;

thus RenField r is add-associative :: thesis: ( RenField r is right_zeroed & RenField r is right_complementable )

proof

now :: thesis: for a, b, c being Element of (RenField r) holds (a + b) + c = a + (b + c)

let a, b, c be Element of (RenField r); :: thesis: (a + b) + c = a + (b + c)
reconsider a1 = a, b1 = b, c1 = c as Element of rng r by defrf;
H: dom r = the carrier of F by defr;
then reconsider ab = r . (((r ") . a1) + ((r ") . b1)), bc = r . (((r ") . b1) + ((r ") . c1)) as Element of rng r by FUNCT_1:3;
thus (a + b) + c = (ren_add r) . ((a + b),c) by defrf
.= (ren_add r) . (((ren_add r) . (a,b)),c) by defrf
.= (ren_add r) . ((r . (((r ") . a1) + ((r ") . b1))),c) by defra
.= r . (((r ") . ab) + ((r ") . c1)) by defra
.= r . ((((r ") . a1) + ((r ") . b1)) + ((r ") . c1)) by H, FUNCT_1:34
.= r . (((r ") . a1) + (((r ") . b1) + ((r ") . c1))) by RLVECT_1:def 3
.= r . (((r ") . a1) + ((r ") . bc)) by H, FUNCT_1:34
.= (ren_add r) . (a,(r . (((r ") . b1) + ((r ") . c1)))) by defra
.= (ren_add r) . (a,((ren_add r) . (b,c))) by defra
.= (ren_add r) . (a,(b + c)) by defrf
.= a + (b + c) by defrf ; :: thesis: verum

end;

hence RenField r is add-associative ; :: thesis: verum

end;

thus RenField r is right_zeroed :: thesis: RenField r is right_complementable

proof

now :: thesis: for a being Element of (RenField r) holds a + (0. (RenField r)) = a

let a be Element of (RenField r); :: thesis: a + (0. (RenField r)) = a
reconsider a1 = a as Element of rng r by defrf;
H0: dom r = the carrier of F by defr;
then reconsider o = r . (0. F) as Element of rng r by FUNCT_1:3;
H1: (r ") . (r . (0. F)) = 0. F by H0, FUNCT_1:34;
thus a + (0. (RenField r)) = (ren_add r) . (a,(0. (RenField r))) by defrf
.= (ren_add r) . (a,(r . (0. F))) by defrf
.= r . (((r ") . a1) + ((r ") . o)) by defra
.= a by H1, FUNCT_1:35 ; :: thesis: verum

end;

hence RenField r is right_zeroed ; :: thesis: verum

end;

thus RenField r is right_complementable :: thesis: verum

proof

now :: thesis: for a being Element of (RenField r) holds a is right_complementable

let a be Element of (RenField r); :: thesis: a is right_complementable
reconsider a1 = a as Element of rng r by defrf;
(r ") . a1 is right_complementable ;
then consider b1 being Element of F such that
H0: ((r ") . a1) + b1 = 0. F ;
H1: rng r = the carrier of (RenField r) by defrf;
H2: dom r = the carrier of F by defr;
then reconsider b = r . b1 as Element of (RenField r) by H1, FUNCT_1:3;
reconsider o = r . b1 as Element of rng r by H2, FUNCT_1:3;
a + b = (ren_add r) . (a,b) by defrf
.= r . (((r ") . a1) + ((r ") . o)) by defra
.= r . (0. F) by H0, H2, FUNCT_1:34
.= 0. (RenField r) by defrf ;
hence a is right_complementable ; :: thesis: verum

end;

hence RenField r is right_complementable ; :: thesis: verum

end;