set C = carrier/\ F;
set f = the addF of F;
carrier/\ F is the addF of F -binopclosed

proof

let x be set ; :: according to REALSET1:def 1 :: thesis: ( not x in [:(carrier/\ F),(carrier/\ F):] or the addF of F . x in carrier/\ F )
assume x in [:(carrier/\ F),(carrier/\ F):] ; :: thesis: the addF of F . x in carrier/\ F
then consider x1, x2 being object such that
A1: x1 in carrier/\ F and
A2: x2 in carrier/\ F and
A3: x = [x1,x2] by ZFMISC_1:def 2;
consider y1 being Element of F such that
A4: x1 = y1 and
A5: for K being Subfield of F holds y1 in K by A1;
consider y2 being Element of F such that
A6: x2 = y2 and
A7: for K being Subfield of F holds y2 in K by A2;

now :: thesis: for K being Subfield of F holds the addF of F . (y1,y2) in K

let K be Subfield of F; :: thesis: the addF of F . (y1,y2) in K
( y1 in K & y2 in K ) by A5, A7;
then reconsider a1 = y1, a2 = y2 as Element of K ;
the addF of K = the addF of F || the carrier of K by EC_PF_1:def 1;
then the addF of K . (a1,a2) = the addF of F . (a1,a2) by Th1;
hence the addF of F . (y1,y2) in K ; :: thesis: verum

end;

hence the addF of F . x in carrier/\ F by A3, A4, A6; :: thesis: verum

end;

then reconsider C = carrier/\ F as Preserv of the addF of F ;
set f = the multF of F;
C is the multF of F -binopclosed

proof

let x be set ; :: according to REALSET1:def 1 :: thesis: ( not x in [:C,C:] or the multF of F . x in C )
assume x in [:C,C:] ; :: thesis: the multF of F . x in C
then consider x1, x2 being object such that
A8: x1 in C and
A9: x2 in C and
A10: x = [x1,x2] by ZFMISC_1:def 2;
consider y1 being Element of F such that
A11: x1 = y1 and
A12: for K being Subfield of F holds y1 in K by A8;
consider y2 being Element of F such that
A13: x2 = y2 and
A14: for K being Subfield of F holds y2 in K by A9;

now :: thesis: for K being Subfield of F holds the multF of F . (y1,y2) in K

let K be Subfield of F; :: thesis: the multF of F . (y1,y2) in K
( y1 in K & y2 in K ) by A12, A14;
then reconsider a1 = y1, a2 = y2 as Element of K ;
the multF of K = the multF of F || the carrier of K by EC_PF_1:def 1;
then the multF of K . (a1,a2) = the multF of F . (a1,a2) by Th1;
hence the multF of F . (y1,y2) in K ; :: thesis: verum

end;

hence the multF of F . x in C by A10, A11, A13; :: thesis: verum

end;

then reconsider D = C as Preserv of the multF of F ;
reconsider m = the multF of F || D as BinOp of C ;
set o = 1. F;
set z = 0. F;

now :: thesis: for K being Subfield of F holds
( 1. F in K & 0. F in K )

let K be Subfield of F; :: thesis: ( 1. F in K & 0. F in K )
( 1. F = 1. K & 0. F = 0. K ) by EC_PF_1:def 1;
hence ( 1. F in K & 0. F in K ) ; :: thesis: verum

end;

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