set B = Polynom-Ring F;
set C = { q where q is Polynomial of F : deg q < deg p } ;
set A = the addF of (Polynom-Ring F);
set M = poly_mult_mod p;
reconsider C1 = { q where q is Polynomial of F : deg q < deg p } as Preserv of the addF of (Polynom-Ring F) by pr1;
reconsider ad = the addF of (Polynom-Ring F) || C1 as BinOp of { q where q is Polynomial of F : deg q < deg p } ;
reconsider C2 = { q where q is Polynomial of F : deg q < deg p } as Preserv of poly_mult_mod p by pr2;
reconsider mu = (poly_mult_mod p) || C2 as BinOp of { q where q is Polynomial of F : deg q < deg p } ;
reconsider O = 1_. F as Element of { q where q is Polynomial of F : deg q < deg p } by pr3;
reconsider Z = 0_. F as Element of { q where q is Polynomial of F : deg q < deg p } by pr4;
take doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) ; :: thesis: ( the carrier of doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) = { q where q is Polynomial of F : deg q < deg p } & the addF of doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) = the addF of (Polynom-Ring F) || the carrier of doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) & the multF of doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) = (poly_mult_mod p) || the carrier of doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) & the OneF of doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) = 1_. F & the ZeroF of doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) = 0_. F )
thus ( the carrier of doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) = { q where q is Polynomial of F : deg q < deg p } & the addF of doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) = the addF of (Polynom-Ring F) || the carrier of doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) & the multF of doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) = (poly_mult_mod p) || the carrier of doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) & the OneF of doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) = 1_. F & the ZeroF of doubleLoopStr(# { q where q is Polynomial of F : deg q < deg p } ,ad,mu,O,Z #) = 0_. F ) ; :: thesis: verum