set C = Alg_El E;
set f = the addF of E;
Alg_El E is Preserv of the addF of E

proof

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

let x be set ; :: thesis: ( x in [:(Alg_El E),(Alg_El E):] implies the addF of E . x in Alg_El E )
assume x in [:(Alg_El E),(Alg_El E):] ; :: thesis: the addF of E . x in Alg_El E
then consider x1, x2 being object such that
A1: x1 in Alg_El E and
A2: x2 in Alg_El E and
A3: x = [x1,x2] by ZFMISC_1:def 2;
consider a1 being F -algebraic Element of E such that
A4: a1 = x1 by A1;
consider a2 being F -algebraic Element of E such that
A5: a2 = x2 by A2;
a1 + a2 = the addF of E . (a1,a2) ;
hence the addF of E . x in Alg_El E by A4, A5, A3; :: thesis: verum

end;

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

end;

then reconsider C = Alg_El E as Preserv of the addF of E ;
set f = the multF of E;

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 a1 being F -algebraic Element of E such that
A4: a1 = x1 by A1;
consider a2 being F -algebraic Element of E such that
A5: a2 = x2 by A2;
a1 * a2 = the multF of E . (a1,a2) ;
hence the multF of E . x in C by A4, A5, A3; :: thesis: verum

end;

then C is the multF of E -binopclosed ;
then reconsider m = the multF of E || C as BinOp of C by REALSET1:2;
( 1. E in C & 0. E in C ) ;
then reconsider o = 1. E, 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 #) = Alg_El E & the addF of doubleLoopStr(# C,( the addF of E || C),m,o,z #) = the addF of E || the carrier of doubleLoopStr(# C,( the addF of E || C),m,o,z #) & the multF of doubleLoopStr(# C,( the addF of E || C),m,o,z #) = the multF of E || the carrier of doubleLoopStr(# C,( the addF of E || C),m,o,z #) & 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 #) = Alg_El E & the addF of doubleLoopStr(# C,( the addF of E || C),m,o,z #) = the addF of E || the carrier of doubleLoopStr(# C,( the addF of E || C),m,o,z #) & the multF of doubleLoopStr(# C,( the addF of E || C),m,o,z #) = the multF of E || the carrier of doubleLoopStr(# C,( the addF of E || C),m,o,z #) & 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