let X be non empty set ; :: thesis: for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let d1, d2 be Element of X; :: thesis: for A being BinOp of X
for M being Function of [:X,X:],X
for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let A be BinOp of X; :: thesis: for M being Function of [:X,X:],X
for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let M be Function of [:X,X:],X; :: thesis: for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let V be Ring; :: thesis: for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let V1 be Subset of V; :: thesis: ( V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse implies doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V )
assume that
A1: V1 = X and
A2: A = the addF of V || V1 and
A3: M = the multF of V || V1 and
A4: d1 = 1. V and
A5: d2 = 0. V and
A6: for v being Element of V st v in V1 holds
- v in V1 ; :: according to C0SP1:def 1 :: thesis: doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
reconsider W = doubleLoopStr(# X,A,M,d1,d2 #) as non empty doubleLoopStr ;

A7: now :: thesis: for a, x being Element of W holds a * x = the multF of V . (a,x)

let a, x be Element of W; :: thesis: a * x = the multF of V . (a,x)
a * x = the multF of V . [a,x] by A1, A3, FUNCT_1:49;
hence a * x = the multF of V . (a,x) ; :: thesis: verum

end;

A8: now :: thesis: for x, y being Element of W holds x + y = the addF of V . (x,y)

let x, y be Element of W; :: thesis: x + y = the addF of V . (x,y)
x + y = the addF of V . [x,y] by A1, A2, FUNCT_1:49;
hence x + y = the addF of V . (x,y) ; :: thesis: verum

end;

A9: ( W is Abelian & W is add-associative & W is right_zeroed & W is right_complementable & W is associative & W is well-unital & W is distributive )

proof

set MV = the multF of V;
set Av = the addF of V;

hereby :: according to RLVECT_1:def 2 :: thesis: ( W is add-associative & W is right_zeroed & W is right_complementable & W is associative & W is well-unital & W is distributive )

let x, y be Element of W; :: thesis: x + y = y + x
reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def 3;
( x + y = x1 + y1 & y + x = y1 + x1 ) by A8;
hence x + y = y + x ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 3 :: thesis: ( W is right_zeroed & W is right_complementable & W is associative & W is well-unital & W is distributive )

let x, y, z be Element of W; :: thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as Element of V by A1, TARSKI:def 3;
x + (y + z) = the addF of V . (x1,(y + z)) by A8;
then A10: x + (y + z) = x1 + (y1 + z1) by A8;
(x + y) + z = the addF of V . ((x + y),z1) by A8;
then (x + y) + z = (x1 + y1) + z1 by A8;
hence (x + y) + z = x + (y + z) by A10, RLVECT_1:def 3; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 4 :: thesis: ( W is right_complementable & W is associative & W is well-unital & W is distributive )

let x be Element of W; :: thesis: x + (0. W) = x
reconsider y = x as Element of V by A1, TARSKI:def 3;
x + (0. W) = y + (0. V) by A5, A8;
hence x + (0. W) = x ; :: thesis: verum

end;

thus W is right_complementable :: thesis: ( W is associative & W is well-unital & W is distributive )

proof

let x be Element of W; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x1 = x as Element of V by A1, TARSKI:def 3;
consider v being Element of V such that
A11: x1 + v = 0. V by ALGSTR_0:def 11;
v = - x1 by A11, VECTSP_1:16;
then reconsider y = v as Element of W by A1, A6;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. W
thus x + y = 0. W by A5, A8, A11; :: thesis: verum

end;

hereby :: according to GROUP_1:def 3 :: thesis: ( W is well-unital & W is distributive )

let a, b, x be Element of W; :: thesis: (a * b) * x = a * (b * x)
reconsider y = x, a1 = a, b1 = b as Element of V by A1, TARSKI:def 3;
a * (b * x) = the multF of V . (a,(b * x)) by A7;
then A12: a * (b * x) = a1 * (b1 * y) by A7;
a * b = a1 * b1 by A7;
then (a * b) * x = (a1 * b1) * y by A7;
hence (a * b) * x = a * (b * x) by A12, GROUP_1:def 3; :: thesis: verum

end;

hereby :: according to VECTSP_1:def 6 :: thesis: W is distributive

let x be Element of W; :: thesis: ( x * (1. W) = x & (1. W) * x = x )
reconsider y = x as Element of V by A1, TARSKI:def 3;
( x * (1. W) = y * (1. V) & (1. W) * x = (1. V) * y ) by A4, A7;
hence ( x * (1. W) = x & (1. W) * x = x ) ; :: thesis: verum

end;

hereby :: according to VECTSP_1:def 7 :: thesis: verum

let a, x, y be Element of W; :: thesis: ( a * (x + y) = (a * x) + (a * y) & (x + y) * a = (x * a) + (y * a) )
reconsider x1 = x, y1 = y, a1 = a as Element of V by A1, TARSKI:def 3;
(x + y) * a = the multF of V . ((x + y),a) by A7;
then (x + y) * a = (x1 + y1) * a1 by A8;
then (x + y) * a = (x1 * a1) + (y1 * a1) by VECTSP_1:def 7;
then (x + y) * a = the addF of V . (( the multF of V . (x1,a1)),(y * a)) by A7;
then A13: (x + y) * a = the addF of V . ((x * a),(y * a)) by A7;
a * (x + y) = the multF of V . (a,(x + y)) by A7;
then a * (x + y) = a1 * (x1 + y1) by A8;
then a * (x + y) = (a1 * x1) + (a1 * y1) by VECTSP_1:def 7;
then a * (x + y) = the addF of V . (( the multF of V . (a,x1)),(a * y)) by A7;
then a * (x + y) = the addF of V . ((a * x),(a * y)) by A7;
hence ( a * (x + y) = (a * x) + (a * y) & (x + y) * a = (x * a) + (y * a) ) by A8, A13; :: thesis: verum

end;

end;

( 0. W = 0. V & 1. W = 1. V ) by A4, A5;
hence doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V by A1, A2, A3, A9, Def3; :: thesis: verum