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
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 & 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 & 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 ;
then A11: a + b = acs . x by ;
(a + b) * s = (s * a) + (s * b) by
.= s * (a + b) by VECTSP_1:def 2 ;
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 & 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 ;
then A19: a * b = mcs . x by ;
(a * b) * s = a * (s * b) by
.= (a * s) * b by GROUP_1:def 3
.= s * (a * b) by ;
hence y in ccs by ; :: thesis: verum
end;
then reconsider mcs = mcs as BinOp of ccs by FUNCT_2:6;
(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 )
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
.= x ; :: thesis: e * x = x
thus e * x = (1. R) * y by
.= x ; :: thesis: verum
end;
A24: cs is well-unital by A20;
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
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;
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
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 ; :: thesis: verum
end;
A29: 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
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 ; :: thesis: verum
end;
A32: 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 A29
.= y + x by A29 ; :: thesis: verum
end;
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;
A34: x9 + y9 = x + y by A29;
A35: y9 + z9 = y + z by A29;
thus (x + y) + z = (x9 + y9) + z9 by
.= x9 + (y9 + z9) by RLVECT_1:def 3
.= x + (y + z) by ; :: thesis: verum
end;
A36: 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 A29
.= x by RLVECT_1:def 4 ; :: thesis: verum
end;
A37: 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
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 ;
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;
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;
A40: 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;
A41: x9 * y9 = x * y by A26;
A42: y9 * z9 = y * z by A26;
thus (x * y) * z = (x9 * y9) * z9 by
.= x9 * (y9 * z9) by GROUP_1:def 3
.= x * (y * z) by ; :: thesis: verum
end;
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 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
.= (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;
A49: 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 A50: 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
A51: y9 * x9 = 1. R by ;
A52: x9 * y9 = 1. R by ;
(1. R) * s = s
.= s * (1. R) ;
then (x9 * y9) * s = (s * x9) * y9 by ;
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 ;
then ((1_ R) * y9) * s = ((1_ R) * s) * y9 by ;
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 ; :: thesis: verum
end;
not cs is degenerated ;
hence ex b1 being strict Skew-Field st
( the carrier of b1 = { x where x is Element of R : x * s = s * x } & the addF of b1 = the addF of R || the carrier of b1 & the multF of b1 = the multF of R || the carrier of b1 & 0. b1 = 0. R & 1. b1 = 1. R ) by A24, A32, A33, A36, A37, A40, A43, A49; :: thesis: verum