let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: doubleLoopStr(# the carrier of (Polynom-Algebra L), the addF of (Polynom-Algebra L), the multF of (Polynom-Algebra L), the OneF of (Polynom-Algebra L), the ZeroF of (Polynom-Algebra L) #) = Polynom-Ring L
A1: ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) & Polynom-Algebra L = GenAlg A ) by Def6;
then A2: the carrier of (Polynom-Algebra L) = the carrier of (Polynom-Ring L) by Th21, Th22;
A3: the carrier of (Polynom-Algebra L) c= the carrier of (Formal-Series L) by A1, Def3;
A4: for x being Element of (Polynom-Algebra L)
for y being Element of (Polynom-Ring L) holds the addF of (Polynom-Algebra L) . (x,y) = the addF of (Polynom-Ring L) . (x,y)

proof

let x be Element of (Polynom-Algebra L); :: thesis: for y being Element of (Polynom-Ring L) holds the addF of (Polynom-Algebra L) . (x,y) = the addF of (Polynom-Ring L) . (x,y)
let y be Element of (Polynom-Ring L); :: thesis: the addF of (Polynom-Algebra L) . (x,y) = the addF of (Polynom-Ring L) . (x,y)
reconsider y1 = y as Element of (Polynom-Algebra L) by A1, Th21, Th22;
reconsider y9 = y1 as Element of (Formal-Series L) by A1, TARSKI:def 3;
reconsider x9 = x as Element of (Formal-Series L) by A3;
reconsider p = x as AlgSequence of L by A2, POLYNOM3:def 10;
reconsider x1 = x as Element of (Polynom-Ring L) by A1, Th21, Th22;
reconsider q = y as AlgSequence of L by POLYNOM3:def 10;
thus the addF of (Polynom-Algebra L) . (x,y) = x + y1
.= x9 + y9 by A1, Th15
.= p + q by Def2
.= x1 + y by POLYNOM3:def 10
.= the addF of (Polynom-Ring L) . (x,y) ; :: thesis: verum

end;

now :: thesis: for x being Element of (Polynom-Algebra L)
for y being Element of (Polynom-Ring L) holds the multF of (Polynom-Algebra L) . (x,y) = the multF of (Polynom-Ring L) . (x,y)

let x be Element of (Polynom-Algebra L); :: thesis: for y being Element of (Polynom-Ring L) holds the multF of (Polynom-Algebra L) . (x,y) = the multF of (Polynom-Ring L) . (x,y)
let y be Element of (Polynom-Ring L); :: thesis: the multF of (Polynom-Algebra L) . (x,y) = the multF of (Polynom-Ring L) . (x,y)
reconsider y1 = y as Element of (Polynom-Algebra L) by A1, Th21, Th22;
reconsider y9 = y1 as Element of (Formal-Series L) by A1, TARSKI:def 3;
reconsider x9 = x as Element of (Formal-Series L) by A3;
reconsider p = x as AlgSequence of L by A2, POLYNOM3:def 10;
reconsider x1 = x as Element of (Polynom-Ring L) by A1, Th21, Th22;
reconsider q = y as AlgSequence of L by POLYNOM3:def 10;
thus the multF of (Polynom-Algebra L) . (x,y) = x * y1
.= x9 * y9 by A1, Th16
.= p *' q by Def2
.= x1 * y by POLYNOM3:def 10
.= the multF of (Polynom-Ring L) . (x,y) ; :: thesis: verum

end;

then A5: the multF of (Polynom-Algebra L) = the multF of (Polynom-Ring L) by A2, BINOP_1:2;
A6: 1. (Polynom-Algebra L) = 1. (Formal-Series L) by A1, Def3
.= 1_. L by Def2
.= 1. (Polynom-Ring L) by POLYNOM3:def 10 ;
0. (Polynom-Algebra L) = 0. (Formal-Series L) by A1, Def3
.= 0_. L by Def2
.= 0. (Polynom-Ring L) by POLYNOM3:def 10 ;
hence doubleLoopStr(# the carrier of (Polynom-Algebra L), the addF of (Polynom-Algebra L), the multF of (Polynom-Algebra L), the OneF of (Polynom-Algebra L), the ZeroF of (Polynom-Algebra L) #) = Polynom-Ring L by A2, A4, A5, A6, BINOP_1:2; :: thesis: verum