set C = S;
set f = the addF of F;
S is Preserv of the addF of F

proof

now :: thesis:

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

end;

hence S is Preserv of the addF of F by REALSET1:def 1; :: thesis:

end;

then reconsider a = the addF of F || S as BinOp of S by REALSET1:2;
set f = the multF of F;

now :: thesis:

let x be set ; :: thesis:
assume x in [:S,S:] ; :: thesis:
then consider x1, x2 being object such that
A1: x1 in S and
A2: x2 in S and
A3: x = [x1,x2] by ZFMISC_1:def 2;
consider a1 being Element of F such that
A4: a1 = x1 by A1;
consider a2 being Element of F such that
A5: a2 = x2 by A2;
a1 * a2 = the multF of F . (a1,a2) ;
hence the multF of F . x in S by A1, A2, A4, A5, A3, IS; :: thesis:

end;

then S is the multF of F -binopclosed ;
then reconsider m = the multF of F || S as BinOp of S by REALSET1:2;
reconsider o = 1. F, z = 0. F as Element of S by IS;
take doubleLoopStr(# S,a,m,o,z #) ; :: thesis:
thus ( the carrier of doubleLoopStr(# S,a,m,o,z #) = S & the addF of doubleLoopStr(# S,a,m,o,z #) = the addF of F || S & the multF of doubleLoopStr(# S,a,m,o,z #) = the multF of F || S & 0. doubleLoopStr(# S,a,m,o,z #) = 0. F & 1. doubleLoopStr(# S,a,m,o,z #) = 1. F ) ; :: thesis: