set C = carrierRA T;
set f = the addF of S;
carrierRA T is Preserv of the addF of S

let x be set ; :: thesis:
assume x in [:(carrierRA T),(carrierRA T):] ; :: thesis:
then consider x1, x2 being object such that
A1: x1 in carrierRA T and
A2: x2 in carrierRA T and
A3: x = [x1,x2] by ZFMISC_1:def 2;
consider y1 being Element of S such that
A4: x1 = y1 and
A5: for U being Subring of S st R is Subring of U & T is Subset of U holds
y1 in U by A1;
consider y2 being Element of S such that
A6: x2 = y2 and
A7: for U being Subring of S st R is Subring of U & T is Subset of U holds
y2 in U by A2;

let U be Subring of S; :: thesis:
assume ( R is Subring of U & T is Subset of U ) ; :: thesis:
then ( y1 in U & y2 in U ) by A5, A7;
then reconsider a1 = y1, a2 = y2 as Element of U ;
the addF of U = the addF of S || the carrier of U by C0SP1:def 3;
then the addF of U . (a1,a2) = the addF of S . (a1,a2) by RING_3:1;
hence the addF of S . (y1,y2) in U ; :: thesis:

end;

end;

end;

then reconsider C = carrierRA T as Preserv of the addF of S ;
set f = the multF of S;
C is Preserv of the multF of S

let x be set ; :: thesis:
assume x in [:C,C:] ; :: thesis:
then consider x1, x2 being object such that
A1: x1 in C and
A2: x2 in C and
A3: x = [x1,x2] by ZFMISC_1:def 2;
consider y1 being Element of S such that
A4: x1 = y1 and
A5: for U being Subring of S st R is Subring of U & T is Subset of U holds
y1 in U by A1;
consider y2 being Element of S such that
A6: x2 = y2 and
A7: for U being Subring of S st R is Subring of U & T is Subset of U holds
y2 in U by A2;

let U be Subring of S; :: thesis:
assume ( R is Subring of U & T is Subset of U ) ; :: thesis:
then ( y1 in U & y2 in U ) by A5, A7;
then reconsider a1 = y1, a2 = y2 as Element of U ;
the multF of U = the multF of S || the carrier of U by C0SP1:def 3;
then the multF of U . (a1,a2) = the multF of S . (a1,a2) by RING_3:1;
hence the multF of S . (y1,y2) in U ; :: thesis:

end;

end;

end;

then reconsider D = C as Preserv of the multF of S ;
reconsider m = the multF of S || D as BinOp of C ;
set o = 1. S;
set z = 0. S;
ex x being Element of S st
( x = 1. S & ( for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U ) )

take 1. S ; :: thesis:

end;

hence ( 1. S = 1. S & ( for U being Subring of S st R is Subring of U & T is Subset of U holds
1. S in U ) ) ; :: thesis:

end;

then 1. S in C ;
then reconsider o = 1. S as Element of C ;
ex x being Element of S st
( x = 0. S & ( for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U ) )

take 0. S ; :: thesis:

end;

hence ( 0. S = 0. S & ( for U being Subring of S st R is Subring of U & T is Subset of U holds
0. S in U ) ) ; :: thesis:

end;

then 0. S in C ;
then reconsider z = 0. S as Element of C ;
take doubleLoopStr(# C,( the addF of S || C),m,o,z #) ; :: thesis:
thus ( the carrier of doubleLoopStr(# C,( the addF of S || C),m,o,z #) = carrierRA T & the addF of doubleLoopStr(# C,( the addF of S || C),m,o,z #) = the addF of S || (carrierRA T) & the multF of doubleLoopStr(# C,( the addF of S || C),m,o,z #) = the multF of S || (carrierRA T) & the OneF of doubleLoopStr(# C,( the addF of S || C),m,o,z #) = 1. S & the ZeroF of doubleLoopStr(# C,( the addF of S || C),m,o,z #) = 0. S ) ; :: thesis: