set K = RenField r;
thus C: RenField r is commutative :: thesis: ( RenField r is associative & RenField r is well-unital & RenField r is distributive & RenField r is almost_left_invertible )

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_mult r) . (a,b) by defrf
.= r . (((r ") . a1) * ((r ") . b1)) by defrm
.= r . (((r ") . b1) * ((r ") . a1)) by GROUP_1:def 12
.= (ren_mult r) . (b,a) by defrm
.= b * a by defrf ; :: thesis: verum

end;

hence RenField r is commutative ; :: thesis: verum

end;

thus RenField r is associative :: thesis: ( RenField r is well-unital & RenField r is distributive & RenField r is almost_left_invertible )

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;
H0: 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_mult r) . ((a * b),c) by defrf
.= (ren_mult r) . (((ren_mult r) . (a,b)),c) by defrf
.= (ren_mult r) . ((r . (((r ") . a1) * ((r ") . b1))),c) by defrm
.= r . (((r ") . ab) * ((r ") . c1)) by defrm
.= r . ((((r ") . a1) * ((r ") . b1)) * ((r ") . c1)) by H0, FUNCT_1:34
.= r . (((r ") . a1) * (((r ") . b1) * ((r ") . c1))) by GROUP_1:def 3
.= r . (((r ") . a1) * ((r ") . bc)) by H0, FUNCT_1:34
.= (ren_mult r) . (a,(r . (((r ") . b1) * ((r ") . c1)))) by defrm
.= (ren_mult r) . (a,((ren_mult r) . (b,c))) by defrm
.= (ren_mult r) . (a,(b * c)) by defrf
.= a * (b * c) by defrf ; :: thesis: verum

end;

hence RenField r is associative ; :: thesis: verum

end;

thus RenField r is well-unital :: thesis: ( RenField r is distributive & RenField r is almost_left_invertible )

proof

now :: thesis: for a being Element of (RenField r) holds
( a * (1. (RenField r)) = a & (1. (RenField r)) * a = a )

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

end;

hence RenField r is well-unital ; :: thesis: verum

end;

thus RenField r is distributive :: thesis: RenField r is almost_left_invertible

proof

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

let a, b, c be Element of (RenField r); :: thesis: (a + b) * c = (a * c) + (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)), ac = r . (((r ") . a1) * ((r ") . c1)), bc = r . (((r ") . b1) * ((r ") . c1)) as Element of rng r by FUNCT_1:3;
thus (a + b) * c = (ren_mult r) . ((a + b),c) by defrf
.= (ren_mult r) . (((ren_add r) . (a,b)),c) by defrf
.= (ren_mult r) . ((r . (((r ") . a1) + ((r ") . b1))),c) by defra
.= r . (((r ") . ab) * ((r ") . c1)) by defrm
.= r . ((((r ") . a1) + ((r ") . b1)) * ((r ") . c1)) by H, FUNCT_1:34
.= r . ((((r ") . a1) * ((r ") . c1)) + (((r ") . b1) * ((r ") . c1))) by VECTSP_1:def 7
.= r . (((r ") . ac) + (((r ") . b1) * ((r ") . c1))) by H, FUNCT_1:34
.= r . (((r ") . ac) + ((r ") . bc)) by H, FUNCT_1:34
.= (ren_add r) . (ac,bc) by defra
.= (ren_add r) . ((r . (((r ") . a1) * ((r ") . c1))),((ren_mult r) . (b,c))) by defrm
.= (ren_add r) . (((ren_mult r) . (a,c)),((ren_mult r) . (b,c))) by defrm
.= (ren_add r) . ((a * c),((ren_mult r) . (b,c))) by defrf
.= (ren_add r) . ((a * c),(b * c)) by defrf
.= (a * c) + (b * c) by defrf ; :: thesis: verum

end;

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

let a, b, c be Element of (RenField r); :: thesis: ( (a + b) * c = (a * c) + (b * c) & a * (b + c) = (a * b) + (a * c) )
thus (a + b) * c = (a * c) + (b * c) by D; :: thesis: a * (b + c) = (a * b) + (a * c)
thus a * (b + c) = (b + c) * a by C
.= (b * a) + (c * a) by D
.= (a * b) + (c * a) by C
.= (a * b) + (a * c) by C ; :: thesis: verum

end;

hence RenField r is distributive ; :: thesis: verum

end;

thus RenField r is almost_left_invertible :: thesis: verum

proof

now :: thesis: for a being Element of (RenField r) st a <> 0. (RenField r) holds
a is left_invertible

let a be Element of (RenField r); :: thesis: ( a <> 0. (RenField r) implies a is left_invertible )
assume AS: a <> 0. (RenField r) ; :: thesis: a is left_invertible
reconsider a1 = a as Element of rng r by defrf;
I0: dom r = the carrier of F by defr;
I1: rng r = the carrier of (RenField r) by defrf;
I2: dom (r ") = rng r by FUNCT_1:33;
0. (RenField r) = r . (0. F) by defrf;
then (r ") . a1 <> (r ") . (r . (0. F)) by I1, I2, AS, FUNCT_1:def 4;
then (r ") . a1 <> 0. F by I0, FUNCT_1:34;
then (r ") . a1 is left_invertible by ALGSTR_0:def 39;
then consider b1 being Element of F such that
H0: b1 * ((r ") . a1) = 1. 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;
b * a = (ren_mult r) . (b,a) by defrf
.= r . (((r ") . o) * ((r ") . a1)) by defrm
.= r . (1. F) by I0, H0, FUNCT_1:34
.= 1. (RenField r) by defrf ;
hence a is left_invertible ; :: thesis: verum

end;

hence RenField r is almost_left_invertible ; :: thesis: verum

end;