let R be non degenerated comRing; ( BSPoly R is one-to-one & BSPoly R is onto )
BSPoly R is onto
proof
for
o being
object st
o in [#] (Polynom-Ring R) holds
o in rng (BSPoly R)
proof
let o be
object ;
( o in [#] (Polynom-Ring R) implies o in rng (BSPoly R) )
assume A1:
o in [#] (Polynom-Ring R)
;
o in rng (BSPoly R)
then A2:
o is
finite-Support sequence of
R
by POLYNOM3:def 10;
o in Formal-Series R
by A2, POLYALG1:def 2;
then consider f1 being
sequence of
R such that A3:
(
f1 = o &
(SBFSeri R) . o = f1 * BagN1 )
by Def5;
f1 is
finite-Support sequence of
R
by A3, A1, POLYNOM3:def 10;
then A4:
Support f1 is
finite
by Th3;
card (Support f1) = card (Support (f1 * BagN1))
by Th41;
then
Support (f1 * BagN1) is
finite
by A4;
then A5:
f1 * BagN1 is
Polynomial of 1,
R
by POLYNOM1:def 5;
then A6:
(SBFSeri R) . o in Polynom-Ring (1,
R)
by A3, POLYNOM1:def 11;
set p =
(SBFSeri R) . o;
dom ((BSFSeri R) * (SBFSeri R)) = [#] (Formal-Series R)
by FUNCT_2:def 1;
then A7:
o in dom ((BSFSeri R) * (SBFSeri R))
by A2, POLYALG1:def 2;
then
o in dom (SBFSeri R)
by FUNCT_2:123;
then
o in dom ((BSFSeri R) ")
by Th32;
then A8:
o in rng (BSFSeri R)
by FUNCT_1:33;
(SBFSeri R) . o in Polynom-Ring (1,
R)
by A5, A3, POLYNOM1:def 11;
then A9:
(SBFSeri R) . o in dom (BSPoly R)
by FUNCT_2:def 1;
(BSPoly R) . ((SBFSeri R) . o) =
(BSFSeri R) . ((SBFSeri R) . o)
by A6, FUNCT_1:49
.=
((BSFSeri R) * (SBFSeri R)) . o
by A7, FUNCT_2:15
.=
((BSFSeri R) * ((BSFSeri R) ")) . o
by Th32
.=
o
by A8, FUNCT_1:35
;
hence
o in rng (BSPoly R)
by A9, FUNCT_1:def 3;
verum
end;
then
[#] (Polynom-Ring R) c= rng (BSPoly R)
;
hence
BSPoly R is
onto
by XBOOLE_0:def 10;
verum
end;
hence
( BSPoly R is one-to-one & BSPoly R is onto )
; verum