let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; 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);
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);
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)
;
verum
end;
now 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);
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);
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)
;
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; verum