set cR = the carrier of R;

set ccs = { x where x is Element of R : for s being Element of R holds x * s = s * x } ;

for s being Element of the carrier of R holds (0. R) * s = s * (0. R) ;

then A1: 0. R in { x where x is Element of R : for s being Element of R holds x * s = s * x } ;

then reconsider ccs = { x where x is Element of R : for s being Element of R holds x * s = s * x } as non empty set ;

A2: ccs c= the carrier of R

set mcs = the multF of R || ccs;

set Zs = 0. R;

set Us = 1_ R;

A3: [:ccs,ccs:] c= [: the carrier of R, the carrier of R:]

rng acs c= ccs

reconsider mcs = the multF of R || ccs as Function of [:ccs,ccs:], the carrier of R by A3, FUNCT_2:32;

rng mcs c= ccs

reconsider Zs = 0. R as Element of ccs by A1;

for s being Element of the carrier of R holds (1_ R) * s = s * (1_ R) ;

then 1_ R in ccs ;

then reconsider Us = 1_ R as Element of ccs ;

reconsider cs = doubleLoopStr(# ccs,acs,mcs,Us,Zs #) as non empty doubleLoopStr ;

set ccs1 = the carrier of cs;

for c, d being Element of the carrier of cs st a = c & b = d holds

a + b = c + d

A43: cs is distributive

take cs ; :: thesis: ( the carrier of cs = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of cs = the addF of R || the carrier of cs & the multF of cs = the multF of R || the carrier of cs & 0. cs = 0. R & 1. cs = 1. R )

thus ( the carrier of cs = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of cs = the addF of R || the carrier of cs & the multF of cs = the multF of R || the carrier of cs & 0. cs = 0. R & 1. cs = 1. R ) ; :: thesis: verum

set ccs = { x where x is Element of R : for s being Element of R holds x * s = s * x } ;

for s being Element of the carrier of R holds (0. R) * s = s * (0. R) ;

then A1: 0. R in { x where x is Element of R : for s being Element of R holds x * s = s * x } ;

then reconsider ccs = { x where x is Element of R : for s being Element of R holds x * s = s * x } as non empty set ;

A2: ccs c= the carrier of R

proof

set acs = the addF of R || ccs;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ccs or x in the carrier of R )

assume x in ccs ; :: thesis: x in the carrier of R

then ex x9 being Element of the carrier of R st

( x9 = x & ( for s being Element of R holds x9 * s = s * x9 ) ) ;

hence x in the carrier of R ; :: thesis: verum

end;assume x in ccs ; :: thesis: x in the carrier of R

then ex x9 being Element of the carrier of R st

( x9 = x & ( for s being Element of R holds x9 * s = s * x9 ) ) ;

hence x in the carrier of R ; :: thesis: verum

set mcs = the multF of R || ccs;

set Zs = 0. R;

set Us = 1_ R;

A3: [:ccs,ccs:] c= [: the carrier of R, the carrier of R:]

proof

then reconsider acs = the addF of R || ccs as Function of [:ccs,ccs:], the carrier of R by FUNCT_2:32;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:ccs,ccs:] or x in [: the carrier of R, the carrier of R:] )

assume x in [:ccs,ccs:] ; :: thesis: x in [: the carrier of R, the carrier of R:]

then ex a, b being object st

( a in ccs & b in ccs & x = [a,b] ) by ZFMISC_1:def 2;

hence x in [: the carrier of R, the carrier of R:] by A2, ZFMISC_1:def 2; :: thesis: verum

end;assume x in [:ccs,ccs:] ; :: thesis: x in [: the carrier of R, the carrier of R:]

then ex a, b being object st

( a in ccs & b in ccs & x = [a,b] ) by ZFMISC_1:def 2;

hence x in [: the carrier of R, the carrier of R:] by A2, ZFMISC_1:def 2; :: thesis: verum

rng acs c= ccs

proof

then reconsider acs = acs as BinOp of ccs by FUNCT_2:6;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng acs or y in ccs )

assume y in rng acs ; :: thesis: y in ccs

then consider x being object such that

A4: x in dom acs and

A5: y = acs . x by FUNCT_1:def 3;

consider a, b being object such that

A6: a in ccs and

A7: b in ccs and

A8: x = [a,b] by A4, ZFMISC_1:def 2;

reconsider a = a, b = b as Element of the carrier of R by A2, A6, A7;

A9: ex a9 being Element of the carrier of R st

( a9 = a & ( for s being Element of R holds a9 * s = s * a9 ) ) by A6;

A10: ex b9 being Element of the carrier of R st

( b9 = b & ( for s being Element of R holds b9 * s = s * b9 ) ) by A7;

[a,b] in [:ccs,ccs:] by A6, A7, ZFMISC_1:def 2;

then A11: a + b = acs . x by A8, FUNCT_1:49;

end;assume y in rng acs ; :: thesis: y in ccs

then consider x being object such that

A4: x in dom acs and

A5: y = acs . x by FUNCT_1:def 3;

consider a, b being object such that

A6: a in ccs and

A7: b in ccs and

A8: x = [a,b] by A4, ZFMISC_1:def 2;

reconsider a = a, b = b as Element of the carrier of R by A2, A6, A7;

A9: ex a9 being Element of the carrier of R st

( a9 = a & ( for s being Element of R holds a9 * s = s * a9 ) ) by A6;

A10: ex b9 being Element of the carrier of R st

( b9 = b & ( for s being Element of R holds b9 * s = s * b9 ) ) by A7;

[a,b] in [:ccs,ccs:] by A6, A7, ZFMISC_1:def 2;

then A11: a + b = acs . x by A8, FUNCT_1:49;

now :: thesis: for s being Element of the carrier of R holds (a + b) * s = s * (a + b)

hence
y in ccs
by A5, A11; :: thesis: verumlet s be Element of the carrier of R; :: thesis: (a + b) * s = s * (a + b)

thus (a + b) * s = (a * s) + (b * s) by VECTSP_1:def 3

.= (s * a) + (b * s) by A9

.= (s * a) + (s * b) by A10

.= s * (a + b) by VECTSP_1:def 2 ; :: thesis: verum

end;thus (a + b) * s = (a * s) + (b * s) by VECTSP_1:def 3

.= (s * a) + (b * s) by A9

.= (s * a) + (s * b) by A10

.= s * (a + b) by VECTSP_1:def 2 ; :: thesis: verum

reconsider mcs = the multF of R || ccs as Function of [:ccs,ccs:], the carrier of R by A3, FUNCT_2:32;

rng mcs c= ccs

proof

then reconsider mcs = mcs as BinOp of ccs by FUNCT_2:6;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng mcs or y in ccs )

assume y in rng mcs ; :: thesis: y in ccs

then consider x being object such that

A12: x in dom mcs and

A13: y = mcs . x by FUNCT_1:def 3;

consider a, b being object such that

A14: a in ccs and

A15: b in ccs and

A16: x = [a,b] by A12, ZFMISC_1:def 2;

reconsider a = a, b = b as Element of the carrier of R by A2, A14, A15;

A17: ex a9 being Element of the carrier of R st

( a9 = a & ( for s being Element of R holds a9 * s = s * a9 ) ) by A14;

A18: ex b9 being Element of the carrier of R st

( b9 = b & ( for s being Element of R holds b9 * s = s * b9 ) ) by A15;

[a,b] in [:ccs,ccs:] by A14, A15, ZFMISC_1:def 2;

then A19: a * b = mcs . x by A16, FUNCT_1:49;

end;assume y in rng mcs ; :: thesis: y in ccs

then consider x being object such that

A12: x in dom mcs and

A13: y = mcs . x by FUNCT_1:def 3;

consider a, b being object such that

A14: a in ccs and

A15: b in ccs and

A16: x = [a,b] by A12, ZFMISC_1:def 2;

reconsider a = a, b = b as Element of the carrier of R by A2, A14, A15;

A17: ex a9 being Element of the carrier of R st

( a9 = a & ( for s being Element of R holds a9 * s = s * a9 ) ) by A14;

A18: ex b9 being Element of the carrier of R st

( b9 = b & ( for s being Element of R holds b9 * s = s * b9 ) ) by A15;

[a,b] in [:ccs,ccs:] by A14, A15, ZFMISC_1:def 2;

then A19: a * b = mcs . x by A16, FUNCT_1:49;

now :: thesis: for s being Element of the carrier of R holds (a * b) * s = s * (a * b)

hence
y in ccs
by A13, A19; :: thesis: verumlet s be Element of the carrier of R; :: thesis: (a * b) * s = s * (a * b)

thus (a * b) * s = a * (b * s) by GROUP_1:def 3

.= a * (s * b) by A18

.= (a * s) * b by GROUP_1:def 3

.= (s * a) * b by A17

.= s * (a * b) by GROUP_1:def 3 ; :: thesis: verum

end;thus (a * b) * s = a * (b * s) by GROUP_1:def 3

.= a * (s * b) by A18

.= (a * s) * b by GROUP_1:def 3

.= (s * a) * b by A17

.= s * (a * b) by GROUP_1:def 3 ; :: thesis: verum

reconsider Zs = 0. R as Element of ccs by A1;

for s being Element of the carrier of R holds (1_ R) * s = s * (1_ R) ;

then 1_ R in ccs ;

then reconsider Us = 1_ R as Element of ccs ;

reconsider cs = doubleLoopStr(# ccs,acs,mcs,Us,Zs #) as non empty doubleLoopStr ;

set ccs1 = the carrier of cs;

A20: now :: thesis: for x, s being Element of the carrier of R st x in ccs holds

x * s = s * x

x * s = s * x

let x, s be Element of the carrier of R; :: thesis: ( x in ccs implies x * s = s * x )

assume x in ccs ; :: thesis: x * s = s * x

then ex x9 being Element of the carrier of R st

( x9 = x & ( for s being Element of R holds x9 * s = s * x9 ) ) ;

hence x * s = s * x ; :: thesis: verum

end;assume x in ccs ; :: thesis: x * s = s * x

then ex x9 being Element of the carrier of R st

( x9 = x & ( for s being Element of R holds x9 * s = s * x9 ) ) ;

hence x * s = s * x ; :: thesis: verum

A21: now :: thesis: for a, b being Element of the carrier of R

for c, d being Element of the carrier of cs st a = c & b = d holds

a * b = c * d

A24:
for a, b being Element of the carrier of Rfor c, d being Element of the carrier of cs st a = c & b = d holds

a * b = c * d

let a, b be Element of the carrier of R; :: thesis: for c, d being Element of the carrier of cs st a = c & b = d holds

a * b = c * d

let c, d be Element of the carrier of cs; :: thesis: ( a = c & b = d implies a * b = c * d )

assume that

A22: a = c and

A23: b = d ; :: thesis: a * b = c * d

[c,d] in [:ccs,ccs:] by ZFMISC_1:def 2;

hence a * b = c * d by A22, A23, FUNCT_1:49; :: thesis: verum

end;a * b = c * d

let c, d be Element of the carrier of cs; :: thesis: ( a = c & b = d implies a * b = c * d )

assume that

A22: a = c and

A23: b = d ; :: thesis: a * b = c * d

[c,d] in [:ccs,ccs:] by ZFMISC_1:def 2;

hence a * b = c * d by A22, A23, FUNCT_1:49; :: thesis: verum

for c, d being Element of the carrier of cs st a = c & b = d holds

a + b = c + d

proof

A27:
cs is Abelian
let a, b be Element of the carrier of R; :: thesis: for c, d being Element of the carrier of cs st a = c & b = d holds

a + b = c + d

let c, d be Element of the carrier of cs; :: thesis: ( a = c & b = d implies a + b = c + d )

assume that

A25: a = c and

A26: b = d ; :: thesis: a + b = c + d

[c,d] in [:ccs,ccs:] by ZFMISC_1:def 2;

hence a + b = c + d by A25, A26, FUNCT_1:49; :: thesis: verum

end;a + b = c + d

let c, d be Element of the carrier of cs; :: thesis: ( a = c & b = d implies a + b = c + d )

assume that

A25: a = c and

A26: b = d ; :: thesis: a + b = c + d

[c,d] in [:ccs,ccs:] by ZFMISC_1:def 2;

hence a + b = c + d by A25, A26, FUNCT_1:49; :: thesis: verum

proof

A28:
cs is add-associative
let x, y be Element of the carrier of cs; :: according to RLVECT_1:def 2 :: thesis: x + y = y + x

reconsider x9 = x, y9 = y as Element of the carrier of R by A2;

thus x + y = y9 + x9 by A24

.= y + x by A24 ; :: thesis: verum

end;reconsider x9 = x, y9 = y as Element of the carrier of R by A2;

thus x + y = y9 + x9 by A24

.= y + x by A24 ; :: thesis: verum

proof

A31:
cs is right_zeroed
let x, y, z be Element of the carrier of cs; :: according to RLVECT_1:def 3 :: thesis: (x + y) + z = x + (y + z)

reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R by A2;

A29: x9 + y9 = x + y by A24;

A30: y9 + z9 = y + z by A24;

thus (x + y) + z = (x9 + y9) + z9 by A24, A29

.= x9 + (y9 + z9) by RLVECT_1:def 3

.= x + (y + z) by A24, A30 ; :: thesis: verum

end;reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R by A2;

A29: x9 + y9 = x + y by A24;

A30: y9 + z9 = y + z by A24;

thus (x + y) + z = (x9 + y9) + z9 by A24, A29

.= x9 + (y9 + z9) by RLVECT_1:def 3

.= x + (y + z) by A24, A30 ; :: thesis: verum

proof

A32:
cs is right_complementable
let x be Element of the carrier of cs; :: according to RLVECT_1:def 4 :: thesis: x + (0. cs) = x

reconsider x9 = x as Element of the carrier of R by A2;

thus x + (0. cs) = x9 + (0. R) by A24

.= x by RLVECT_1:def 4 ; :: thesis: verum

end;reconsider x9 = x as Element of the carrier of R by A2;

thus x + (0. cs) = x9 + (0. R) by A24

.= x by RLVECT_1:def 4 ; :: thesis: verum

proof

A35:
cs is associative
let x be Element of the carrier of cs; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable

reconsider x9 = x as Element of the carrier of R by A2;

consider y9 being Element of the carrier of R such that

A33: x9 + y9 = 0. R by ALGSTR_0:def 11;

then reconsider y = y9 as Element of the carrier of cs ;

x9 + y9 = x + y by A24;

hence ex y being Element of the carrier of cs st x + y = 0. cs by A33; :: according to ALGSTR_0:def 11 :: thesis: verum

end;reconsider x9 = x as Element of the carrier of R by A2;

consider y9 being Element of the carrier of R such that

A33: x9 + y9 = 0. R by ALGSTR_0:def 11;

now :: thesis: for s being Element of the carrier of R holds y9 * s = s * y9

then
y9 in the carrier of cs
;let s be Element of the carrier of R; :: thesis: y9 * s = s * y9

A34: s * x9 = x9 * s by A20;

(0. R) * s = s * (0. R) ;

then (x9 * s) + (y9 * s) = s * (x9 + y9) by A33, VECTSP_1:def 3;

then (x9 * s) + (y9 * s) = (s * x9) + (s * y9) by VECTSP_1:def 2;

then ((- (x9 * s)) + (x9 * s)) + (y9 * s) = (- (s * x9)) + ((s * x9) + (s * y9)) by A34, RLVECT_1:def 3;

then (0. R) + (y9 * s) = (- (s * x9)) + ((s * x9) + (s * y9)) by RLVECT_1:5;

then y9 * s = (- (s * x9)) + ((s * x9) + (s * y9)) by RLVECT_1:4;

then y9 * s = ((- (s * x9)) + (s * x9)) + (s * y9) by RLVECT_1:def 3;

then y9 * s = (0. R) + (s * y9) by RLVECT_1:5;

hence y9 * s = s * y9 by RLVECT_1:4; :: thesis: verum

end;A34: s * x9 = x9 * s by A20;

(0. R) * s = s * (0. R) ;

then (x9 * s) + (y9 * s) = s * (x9 + y9) by A33, VECTSP_1:def 3;

then (x9 * s) + (y9 * s) = (s * x9) + (s * y9) by VECTSP_1:def 2;

then ((- (x9 * s)) + (x9 * s)) + (y9 * s) = (- (s * x9)) + ((s * x9) + (s * y9)) by A34, RLVECT_1:def 3;

then (0. R) + (y9 * s) = (- (s * x9)) + ((s * x9) + (s * y9)) by RLVECT_1:5;

then y9 * s = (- (s * x9)) + ((s * x9) + (s * y9)) by RLVECT_1:4;

then y9 * s = ((- (s * x9)) + (s * x9)) + (s * y9) by RLVECT_1:def 3;

then y9 * s = (0. R) + (s * y9) by RLVECT_1:5;

hence y9 * s = s * y9 by RLVECT_1:4; :: thesis: verum

then reconsider y = y9 as Element of the carrier of cs ;

x9 + y9 = x + y by A24;

hence ex y being Element of the carrier of cs st x + y = 0. cs by A33; :: according to ALGSTR_0:def 11 :: thesis: verum

proof

A38:
cs is commutative
let x, y, z be Element of the carrier of cs; :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)

reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R by A2;

A36: x9 * y9 = x * y by A21;

A37: y9 * z9 = y * z by A21;

thus (x * y) * z = (x9 * y9) * z9 by A21, A36

.= x9 * (y9 * z9) by GROUP_1:def 3

.= x * (y * z) by A21, A37 ; :: thesis: verum

end;reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R by A2;

A36: x9 * y9 = x * y by A21;

A37: y9 * z9 = y * z by A21;

thus (x * y) * z = (x9 * y9) * z9 by A21, A36

.= x9 * (y9 * z9) by GROUP_1:def 3

.= x * (y * z) by A21, A37 ; :: thesis: verum

proof

let x, y be Element of the carrier of cs; :: according to GROUP_1:def 12 :: thesis: x * y = y * x

reconsider x9 = x, y9 = y as Element of the carrier of R by A2;

thus x * y = x9 * y9 by A21

.= y9 * x9 by A20

.= y * x by A21 ; :: thesis: verum

end;reconsider x9 = x, y9 = y as Element of the carrier of R by A2;

thus x * y = x9 * y9 by A21

.= y9 * x9 by A20

.= y * x by A21 ; :: thesis: verum

A39: now :: thesis: for x, e being Element of cs st e = 1_ R holds

( x * e = x & e * x = x )

A42:
cs is well-unital
by A39;( x * e = x & e * x = x )

let x, e be Element of cs; :: thesis: ( e = 1_ R implies ( x * e = x & e * x = x ) )

assume A40: e = 1_ R ; :: thesis: ( x * e = x & e * x = x )

A41: [x,e] in [:ccs,ccs:] by ZFMISC_1:87;

reconsider y = x as Element of R by A2;

thus x * e = y * (1_ R) by A40, A41, FUNCT_1:49

.= x ; :: thesis: e * x = x

hence e * x = x by A38; :: thesis: verum

end;assume A40: e = 1_ R ; :: thesis: ( x * e = x & e * x = x )

A41: [x,e] in [:ccs,ccs:] by ZFMISC_1:87;

reconsider y = x as Element of R by A2;

thus x * e = y * (1_ R) by A40, A41, FUNCT_1:49

.= x ; :: thesis: e * x = x

hence e * x = x by A38; :: thesis: verum

A43: cs is distributive

proof

cs is almost_left_invertible
let x, y, z be Element of the carrier of cs; :: according to VECTSP_1:def 7 :: thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )

reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R by A2;

A44: y + z = y9 + z9 by A24;

A45: x9 * y9 = x * y by A21;

A46: x9 * z9 = x * z by A21;

A47: y9 * x9 = y * x by A21;

A48: z9 * x9 = z * x by A21;

thus x * (y + z) = x9 * (y9 + z9) by A21, A44

.= (x9 * y9) + (x9 * z9) by VECTSP_1:def 7

.= (x * y) + (x * z) by A24, A45, A46 ; :: thesis: (y + z) * x = (y * x) + (z * x)

thus (y + z) * x = (y9 + z9) * x9 by A21, A44

.= (y9 * x9) + (z9 * x9) by VECTSP_1:def 7

.= (y * x) + (z * x) by A24, A47, A48 ; :: thesis: verum

end;reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R by A2;

A44: y + z = y9 + z9 by A24;

A45: x9 * y9 = x * y by A21;

A46: x9 * z9 = x * z by A21;

A47: y9 * x9 = y * x by A21;

A48: z9 * x9 = z * x by A21;

thus x * (y + z) = x9 * (y9 + z9) by A21, A44

.= (x9 * y9) + (x9 * z9) by VECTSP_1:def 7

.= (x * y) + (x * z) by A24, A45, A46 ; :: thesis: (y + z) * x = (y * x) + (z * x)

thus (y + z) * x = (y9 + z9) * x9 by A21, A44

.= (y9 * x9) + (z9 * x9) by VECTSP_1:def 7

.= (y * x) + (z * x) by A24, A47, A48 ; :: thesis: verum

proof

then reconsider cs = cs as strict Field by A27, A28, A31, A32, A35, A38, A42, A43, STRUCT_0:def 8;
let x be Element of the carrier of cs; :: according to ALGSTR_0:def 38 :: thesis: ( x = 0. cs or x is left_invertible )

assume A49: x <> 0. cs ; :: thesis: x is left_invertible

reconsider x9 = x as Element of the carrier of R by A2;

consider y9 being Element of the carrier of R such that

A50: y9 * x9 = 1. R by A49, VECTSP_1:def 9;

A51: x9 * y9 = 1. R by A50, VECTSP_2:7;

then reconsider y = y9 as Element of the carrier of cs ;

take y ; :: according to ALGSTR_0:def 27 :: thesis: y * x = 1. cs

thus y * x = 1. cs by A21, A50; :: thesis: verum

end;assume A49: x <> 0. cs ; :: thesis: x is left_invertible

reconsider x9 = x as Element of the carrier of R by A2;

consider y9 being Element of the carrier of R such that

A50: y9 * x9 = 1. R by A49, VECTSP_1:def 9;

A51: x9 * y9 = 1. R by A50, VECTSP_2:7;

now :: thesis: for s being Element of the carrier of R holds y9 * s = s * y9

then
y9 in the carrier of cs
;let s be Element of the carrier of R; :: thesis: y9 * s = s * y9

(1_ R) * s = s

.= s * (1_ R) ;

then (x9 * y9) * s = (s * x9) * y9 by A51, GROUP_1:def 3;

then (x9 * y9) * s = (x9 * s) * y9 by A20;

then ((x9 ") * (x9 * y9)) * s = (x9 ") * ((x9 * s) * y9) by GROUP_1:def 3;

then ((x9 ") * (x9 * y9)) * s = ((x9 ") * (x9 * s)) * y9 by GROUP_1:def 3;

then (((x9 ") * x9) * y9) * s = ((x9 ") * (x9 * s)) * y9 by GROUP_1:def 3;

then (((x9 ") * x9) * y9) * s = (((x9 ") * x9) * s) * y9 by GROUP_1:def 3;

then ((1_ R) * y9) * s = (((x9 ") * x9) * s) * y9 by A49, VECTSP_2:9;

then ((1_ R) * y9) * s = ((1_ R) * s) * y9 by A49, VECTSP_2:9;

then y9 * s = ((1_ R) * s) * y9 ;

hence y9 * s = s * y9 ; :: thesis: verum

end;(1_ R) * s = s

.= s * (1_ R) ;

then (x9 * y9) * s = (s * x9) * y9 by A51, GROUP_1:def 3;

then (x9 * y9) * s = (x9 * s) * y9 by A20;

then ((x9 ") * (x9 * y9)) * s = (x9 ") * ((x9 * s) * y9) by GROUP_1:def 3;

then ((x9 ") * (x9 * y9)) * s = ((x9 ") * (x9 * s)) * y9 by GROUP_1:def 3;

then (((x9 ") * x9) * y9) * s = ((x9 ") * (x9 * s)) * y9 by GROUP_1:def 3;

then (((x9 ") * x9) * y9) * s = (((x9 ") * x9) * s) * y9 by GROUP_1:def 3;

then ((1_ R) * y9) * s = (((x9 ") * x9) * s) * y9 by A49, VECTSP_2:9;

then ((1_ R) * y9) * s = ((1_ R) * s) * y9 by A49, VECTSP_2:9;

then y9 * s = ((1_ R) * s) * y9 ;

hence y9 * s = s * y9 ; :: thesis: verum

then reconsider y = y9 as Element of the carrier of cs ;

take y ; :: according to ALGSTR_0:def 27 :: thesis: y * x = 1. cs

thus y * x = 1. cs by A21, A50; :: thesis: verum

take cs ; :: thesis: ( the carrier of cs = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of cs = the addF of R || the carrier of cs & the multF of cs = the multF of R || the carrier of cs & 0. cs = 0. R & 1. cs = 1. R )

thus ( the carrier of cs = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of cs = the addF of R || the carrier of cs & the multF of cs = the multF of R || the carrier of cs & 0. cs = 0. R & 1. cs = 1. R ) ; :: thesis: verum