set PR1 = Polynom-Ring (1,R);
set PR = Polynom-Ring R;
set FS1 = Formal-Series (1,R);
set FS = Formal-Series R;
the carrier of (Polynom-Ring (1,R)) c= the carrier of (Formal-Series (1,R))
by Lm7;
then
[#] (Polynom-Ring (1,R)) c= dom (BSFSeri R)
by FUNCT_2:def 1;
then A1:
dom ((BSFSeri R) | ([#] (Polynom-Ring (1,R)))) = [#] (Polynom-Ring (1,R))
by RELAT_1:62;
for o being object st o in the carrier of (Polynom-Ring (1,R)) holds
((BSFSeri R) | ([#] (Polynom-Ring (1,R)))) . o in the carrier of (Polynom-Ring R)
proof
let o be
object ;
( o in the carrier of (Polynom-Ring (1,R)) implies ((BSFSeri R) | ([#] (Polynom-Ring (1,R)))) . o in the carrier of (Polynom-Ring R) )
assume A2:
o in the
carrier of
(Polynom-Ring (1,R))
;
((BSFSeri R) | ([#] (Polynom-Ring (1,R)))) . o in the carrier of (Polynom-Ring R)
then A3:
((BSFSeri R) | ([#] (Polynom-Ring (1,R)))) . o = (BSFSeri R) . o
by FUNCT_1:49;
A4:
o is
finite-Support Series of 1,
R
by A2, POLYNOM1:def 11;
then A5:
o in the
carrier of
(Formal-Series (1,R))
by Def3;
reconsider f =
o as
Element of
(Formal-Series (1,R)) by A4, Def3;
consider x1 being
Series of 1,
R such that A6:
(
x1 = o &
(BSFSeri R) . o = x1 * NBag1 )
by A5, Def4;
card (Support x1) = card (Support (x1 * NBag1))
by Th44;
then
Support (x1 * NBag1) is
finite
by A4, A6;
then
(BSFSeri R) . o is
Polynomial of
R
by A6, Th2;
hence
((BSFSeri R) | ([#] (Polynom-Ring (1,R)))) . o in the
carrier of
(Polynom-Ring R)
by A3, POLYNOM3:def 10;
verum
end;
hence
(BSFSeri R) | ([#] (Polynom-Ring (1,R))) is Function of (Polynom-Ring (1,R)),(Polynom-Ring R)
by A1, FUNCT_2:3; verum