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
consider A being non empty Subset of (Formal-Series L) such that
A1:
( A = the carrier of (Polynom-Ring L) & Polynom-Algebra L = GenAlg A )
by Def6;
A2:
the carrier of (Polynom-Algebra L) = the carrier of (Polynom-Ring L)
by A1, Th22, Th23;
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,ylet 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 x1 =
x as
Element of
(Polynom-Ring L) by A1, Th22, Th23;
reconsider y1 =
y as
Element of
(Polynom-Algebra L) by A1, Th22, Th23;
reconsider x' =
x as
Element of
(Formal-Series L) by A3, TARSKI:def 3;
reconsider y' =
y1 as
Element of
(Formal-Series L) by A1, TARSKI:def 3;
reconsider p =
x as
AlgSequence of
L by A2, POLYNOM3:def 12;
reconsider q =
y as
AlgSequence of
L by POLYNOM3:def 12;
thus the
addF of
(Polynom-Algebra L) . x,
y =
x + y1
.=
x' + y'
by A1, Th15
.=
p + q
by Def2
.=
x1 + y
by POLYNOM3:def 12
.=
the
addF of
(Polynom-Ring L) . x,
y
;
:: thesis: verum
end;
now 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,ylet y be
Element of
(Polynom-Ring L);
:: thesis: the multF of (Polynom-Algebra L) . x,y = the multF of (Polynom-Ring L) . x,yreconsider x1 =
x as
Element of
(Polynom-Ring L) by A1, Th22, Th23;
reconsider y1 =
y as
Element of
(Polynom-Algebra L) by A1, Th22, Th23;
reconsider x' =
x as
Element of
(Formal-Series L) by A3, TARSKI:def 3;
reconsider y' =
y1 as
Element of
(Formal-Series L) by A1, TARSKI:def 3;
reconsider p =
x as
AlgSequence of
L by A2, POLYNOM3:def 12;
reconsider q =
y as
AlgSequence of
L by POLYNOM3:def 12;
thus the
multF of
(Polynom-Algebra L) . x,
y =
x * y1
.=
x' * y'
by A1, Th16
.=
p *' q
by Def2
.=
x1 * y
by POLYNOM3:def 12
.=
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: 0. (Polynom-Algebra L) =
0. (Formal-Series L)
by A1, Def3
.=
0_. L
by Def2
.=
0. (Polynom-Ring L)
by POLYNOM3:def 12
;
1. (Polynom-Algebra L) =
1. (Formal-Series L)
by A1, Def3
.=
1_. L
by Def2
.=
1. (Polynom-Ring L)
by POLYNOM3:def 12
;
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