set C = carrierFA T;
set f = the addF of E;
carrierFA T is Preserv of the addF of E

proof

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

let x be set ; :: thesis: ( x in [:(carrierFA T),(carrierFA T):] implies the addF of E . x in carrierFA T )
assume x in [:(carrierFA T),(carrierFA T):] ; :: thesis: the addF of E . x in carrierFA T
then consider x1, x2 being object such that
A1: x1 in carrierFA T and
A2: x2 in carrierFA T and
A3: x = [x1,x2] by ZFMISC_1:def 2;
consider y1 being Element of E such that
A4: x1 = y1 and
A5: for U being Subfield of E st F is Subfield of U & T is Subset of U holds
y1 in U by A1;
consider y2 being Element of E such that
A6: x2 = y2 and
A7: for U being Subfield of E st F is Subfield of U & T is Subset of U holds
y2 in U by A2;

now :: thesis: for U being Subfield of E st F is Subfield of U & T is Subset of U holds
the addF of E . (y1,y2) in U

let U be Subfield of E; :: thesis: ( F is Subfield of U & T is Subset of U implies the addF of E . (y1,y2) in U )
assume ( F is Subfield of U & T is Subset of U ) ; :: thesis: the addF of E . (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 E || the carrier of U by EC_PF_1:def 1;
then the addF of U . (a1,a2) = the addF of E . (a1,a2) by RING_3:1;
hence the addF of E . (y1,y2) in U ; :: thesis: verum

end;

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

end;

hence carrierFA T is Preserv of the addF of E by REALSET1:def 1; :: thesis: verum

end;

then reconsider C = carrierFA T as Preserv of the addF of E ;
set f = the multF of E;
C is Preserv of the multF of E

proof

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

let x be set ; :: thesis: ( x in [:C,C:] implies the multF of E . x in C )
assume x in [:C,C:] ; :: thesis: the multF of E . 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 E such that
A4: x1 = y1 and
A5: for U being Subfield of E st F is Subfield of U & T is Subset of U holds
y1 in U by A1;
consider y2 being Element of E such that
A6: x2 = y2 and
A7: for U being Subfield of E st F is Subfield of U & T is Subset of U holds
y2 in U by A2;

now :: thesis: for U being Subfield of E st F is Subfield of U & T is Subset of U holds
the multF of E . (y1,y2) in U

let U be Subfield of E; :: thesis: ( F is Subfield of U & T is Subset of U implies the multF of E . (y1,y2) in U )
assume ( F is Subfield of U & T is Subset of U ) ; :: thesis: the multF of E . (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 E || the carrier of U by EC_PF_1:def 1;
then the multF of U . (a1,a2) = the multF of E . (a1,a2) by RING_3:1;
hence the multF of E . (y1,y2) in U ; :: thesis: verum

end;

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

end;

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

end;

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

proof

take 1. E ; :: thesis: ( 1. E = 1. E & ( for U being Subfield of E st F is Subfield of U & T is Subset of U holds
1. E in U ) )

now :: thesis: for U being Subfield of E st T is Subset of U holds
1. E in U

let U be Subfield of E; :: thesis: ( T is Subset of U implies 1. E in U )
assume T is Subset of U ; :: thesis: 1. E in U
1. U = 1. E by EC_PF_1:def 1;
hence 1. E in U ; :: thesis: verum

end;

hence ( 1. E = 1. E & ( for U being Subfield of E st F is Subfield of U & T is Subset of U holds
1. E in U ) ) ; :: thesis: verum

end;

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

proof

take 0. E ; :: thesis: ( 0. E = 0. E & ( for U being Subfield of E st F is Subfield of U & T is Subset of U holds
0. E in U ) )

now :: thesis: for U being Subfield of E st F is Subfield of U & T is Subset of U holds
0. E in U

let U be Subfield of E; :: thesis: ( F is Subfield of U & T is Subset of U implies 0. E in U )
assume ( F is Subfield of U & T is Subset of U ) ; :: thesis: 0. E in U
0. U = 0. E by EC_PF_1:def 1;
hence 0. E in U ; :: thesis: verum

end;

hence ( 0. E = 0. E & ( for U being Subfield of E st F is Subfield of U & T is Subset of U holds
0. E in U ) ) ; :: thesis: verum

end;

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