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
proof
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;
set acs = the addF of R || ccs;
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
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 ; :: thesis: verum
end;
then reconsider acs = the addF of R || ccs as Function of [:ccs,ccs:], the carrier of R by FUNCT_2:32;
rng acs c= ccs
proof
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 ;
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 ;
then A11: a + b = acs . x by ;
now :: thesis: for s being Element of the carrier of R holds (a + b) * s = s * (a + b)
let 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;
hence y in ccs by ; :: thesis: verum
end;
then reconsider acs = acs as BinOp of ccs by FUNCT_2:6;
reconsider mcs = the multF of R || ccs as Function of [:ccs,ccs:], the carrier of R by ;
rng mcs c= ccs
proof
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 ;
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 ;
then A19: a * b = mcs . x by ;
now :: thesis: for s being Element of the carrier of R holds (a * b) * s = s * (a * b)
let 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;
hence y in ccs by ; :: thesis: verum
end;
then reconsider mcs = mcs as BinOp of ccs by FUNCT_2:6;
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
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;
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
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 ; :: thesis: verum
end;
A24: 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
proof
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 ; :: thesis: verum
end;
A27: cs is Abelian
proof
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;
A28: cs is add-associative
proof
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
.= x9 + (y9 + z9) by RLVECT_1:def 3
.= x + (y + z) by ; :: thesis: verum
end;
A31: cs is right_zeroed
proof
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;
A32: cs is right_complementable
proof
let x be Element of the carrier of cs; :: according to ALGSTR_0:def 16 :: thesis:
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
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 ;
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 ;
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;
then y9 in the carrier of cs ;
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;
A35: cs is associative
proof
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
.= x9 * (y9 * z9) by GROUP_1:def 3
.= x * (y * z) by ; :: thesis: verum
end;
A38: cs is commutative
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;
A39: now :: thesis: for x, e being Element of cs st e = 1_ R holds
( 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
.= x ; :: thesis: e * x = x
hence e * x = x by A38; :: thesis: verum
end;
A42: cs is well-unital by A39;
A43: cs is distributive
proof
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
.= (x9 * y9) + (x9 * z9) by VECTSP_1:def 7
.= (x * y) + (x * z) by ; :: thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = (y9 + z9) * x9 by
.= (y9 * x9) + (z9 * x9) by VECTSP_1:def 7
.= (y * x) + (z * x) by ; :: thesis: verum
end;
cs is almost_left_invertible
proof
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:
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 ;
A51: x9 * y9 = 1. R by ;
now :: thesis: for s being Element of the carrier of R holds y9 * s = s * y9
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 ;
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 ;
then ((1_ R) * y9) * s = ((1_ R) * s) * y9 by ;
then y9 * s = ((1_ R) * s) * y9 ;
hence y9 * s = s * y9 ; :: thesis: verum
end;
then y9 in the carrier of cs ;
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 ; :: thesis: verum
end;
then reconsider cs = cs as strict Field by ;
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