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

proof

now :: thesis: for x being set st x in [:(carrierRA T),(carrierRA T):] holds
the addF of S . x in carrierRA T

let x be set ; :: thesis: ( x in [:(carrierRA T),(carrierRA T):] implies the addF of S . x in carrierRA T )
assume x in [:(carrierRA T),(carrierRA T):] ; :: thesis: the addF of S . x in carrierRA T
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;

now :: thesis: for U being Subring of S st R is Subring of U & T is Subset of U holds
the addF of S . (y1,y2) in U

let U be Subring of S; :: thesis: ( R is Subring of U & T is Subset of U implies the addF of S . (y1,y2) in U )
assume ( R is Subring of U & T is Subset of U ) ; :: thesis: the addF of S . (y1,y2) in U
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: verum

end;

hence the addF of S . x in carrierRA T by A3, A4, A6; :: thesis: verum

end;

hence carrierRA T is Preserv of the addF of S by REALSET1:def 1; :: thesis: verum

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

proof

now :: thesis: for x being set st x in [:C,C:] holds
the multF of S . x in C

let x be set ; :: thesis: ( x in [:C,C:] implies the multF of S . x in C )
assume x in [:C,C:] ; :: thesis: the multF of S . x in C
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;

now :: thesis: for U being Subring of S st R is Subring of U & T is Subset of U holds
the multF of S . (y1,y2) in U

let U be Subring of S; :: thesis: ( R is Subring of U & T is Subset of U implies the multF of S . (y1,y2) in U )
assume ( R is Subring of U & T is Subset of U ) ; :: thesis: the multF of S . (y1,y2) in U
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: verum

end;

hence the multF of S . x in C by A3, A4, A6; :: thesis: verum

end;

hence C is Preserv of the multF of S by REALSET1:def 1; :: thesis: verum

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 ) )

proof

take 1. S ; :: thesis: ( 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 ) )

now :: thesis: for U being Subring of S st T is Subset of U holds
1. S in U

let U be Subring of S; :: thesis: ( T is Subset of U implies 1. S in U )
assume T is Subset of U ; :: thesis: 1. S in U
1. U = 1. S by C0SP1:def 3;
hence 1. S in U ; :: thesis: verum

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

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 ) )

proof

take 0. S ; :: thesis: ( 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 ) )

now :: thesis: for U being Subring of S st R is Subring of U & T is Subset of U holds
0. S in U

let U be Subring of S; :: thesis: ( R is Subring of U & T is Subset of U implies 0. S in U )
assume ( R is Subring of U & T is Subset of U ) ; :: thesis: 0. S in U
0. U = 0. S by C0SP1:def 3;
hence 0. S in U ; :: thesis: verum

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

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: ( 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 )
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: verum