set cR = the carrier of R;

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

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

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

then reconsider ccs = { x where x is Element of R : 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

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

then 0. R in ccs ;

then reconsider Zs = 0. R as Element of ccs ;

(1. R) * s = 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

hence ex b_{1} being strict Skew-Field st

( the carrier of b_{1} = { x where x is Element of R : x * s = s * x } & the addF of b_{1} = the addF of R || the carrier of b_{1} & the multF of b_{1} = the multF of R || the carrier of b_{1} & 0. b_{1} = 0. R & 1. b_{1} = 1. R )
by A24, A32, A33, A36, A37, A40, A43, A49; :: thesis: verum

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

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

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

then reconsider ccs = { x where x is Element of R : 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 & 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 & 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 & a9 * s = s * a9 ) by A6;

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

( b9 = b & 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;

(a + b) * s = (s * a) + (s * b) by A9, A10, VECTSP_1:def 3

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

hence y in ccs by A5, A11; :: thesis: verum

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 & a9 * s = s * a9 ) by A6;

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

( b9 = b & 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;

(a + b) * s = (s * a) + (s * b) by A9, A10, VECTSP_1:def 3

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

hence y in ccs by A5, A11; :: 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 & a9 * s = s * a9 ) by A14;

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

( b9 = b & 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;

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

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

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

hence y in ccs by A13, A19; :: thesis: verum

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 & a9 * s = s * a9 ) by A14;

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

( b9 = b & 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;

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

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

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

hence y in ccs by A13, A19; :: thesis: verum

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

then 0. R in ccs ;

then reconsider Zs = 0. R as Element of ccs ;

(1. R) * s = 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 ;

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

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

A24:
cs is well-unital
by A20;( 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 A21: e = 1. R ; :: thesis: ( x * e = x & e * x = x )

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

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

reconsider y = x as Element of R by A2;

thus x * e = y * (1. R) by A21, A22, FUNCT_1:49

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

thus e * x = (1. R) * y by A21, A23, FUNCT_1:49

.= x ; :: thesis: verum

end;assume A21: e = 1. R ; :: thesis: ( x * e = x & e * x = x )

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

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

reconsider y = x as Element of R by A2;

thus x * e = y * (1. R) by A21, A22, FUNCT_1:49

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

thus e * x = (1. R) * y by A21, A23, FUNCT_1:49

.= x ; :: thesis: verum

set ccs1 = the carrier of cs;

A25: now :: thesis: for x being Element of the carrier of R st x in ccs holds

x * s = s * x

x * s = s * x

let x 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 & 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 & x9 * s = s * x9 ) ;

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

A26: 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

A29:
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

A27: a = c and

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

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

hence a * b = c * d by A27, A28, 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

A27: a = c and

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

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

hence a * b = c * d by A27, A28, 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

A32:
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

A30: a = c and

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

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

hence a + b = c + d by A30, A31, 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

A30: a = c and

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

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

hence a + b = c + d by A30, A31, FUNCT_1:49; :: thesis: verum

proof

A33:
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 A29

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

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

thus x + y = y9 + x9 by A29

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

proof

A36:
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;

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

A35: y9 + z9 = y + z by A29;

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

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

.= x + (y + z) by A29, A35 ; :: thesis: verum

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

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

A35: y9 + z9 = y + z by A29;

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

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

.= x + (y + z) by A29, A35 ; :: thesis: verum

proof

A37:
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 A29

.= 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 A29

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

proof

A40:
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

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

A39: s * x9 = x9 * s by A25;

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

then (x9 * s) + (y9 * s) = s * (x9 + y9) by A38, 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 A39, 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;

then y9 * s = s * y9 by RLVECT_1:4;

then y9 in the carrier of cs ;

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

x9 + y9 = x + y by A29;

hence ex y being Element of the carrier of cs st x + y = 0. cs by A38; :: 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

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

A39: s * x9 = x9 * s by A25;

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

then (x9 * s) + (y9 * s) = s * (x9 + y9) by A38, 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 A39, 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;

then y9 * s = s * y9 by RLVECT_1:4;

then y9 in the carrier of cs ;

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

x9 + y9 = x + y by A29;

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

proof

A43:
cs is distributive
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;

A41: x9 * y9 = x * y by A26;

A42: y9 * z9 = y * z by A26;

thus (x * y) * z = (x9 * y9) * z9 by A26, A41

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

.= x * (y * z) by A26, A42 ; :: thesis: verum

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

A41: x9 * y9 = x * y by A26;

A42: y9 * z9 = y * z by A26;

thus (x * y) * z = (x9 * y9) * z9 by A26, A41

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

.= x * (y * z) by A26, A42 ; :: thesis: verum

proof

A49:
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 A29;

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

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

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

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

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

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

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

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

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

.= (y * x) + (z * x) by A29, 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 A29;

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

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

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

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

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

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

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

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

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

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

proof

not cs is degenerated
;
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 A50: 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

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

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

(1. R) * s = s

.= s * (1. R) ;

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

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

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 A50, VECTSP_2:9;

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

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

then y9 * s = s * y9 ;

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 A26, A51; :: thesis: verum

end;assume A50: 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

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

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

(1. R) * s = s

.= s * (1. R) ;

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

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

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 A50, VECTSP_2:9;

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

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

then y9 * s = s * y9 ;

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 A26, A51; :: thesis: verum

hence ex b

( the carrier of b