let R be non degenerated comRing; (BSFSeri R) " = SBFSeri R
A1: rng (BSFSeri R) =
the carrier of (Formal-Series R)
by FUNCT_2:def 3
.=
dom (SBFSeri R)
by FUNCT_2:def 1
;
for o being object st o in dom ((SBFSeri R) * (BSFSeri R)) holds
((SBFSeri R) * (BSFSeri R)) . o = (id (dom (BSFSeri R))) . o
proof
let o be
object ;
( o in dom ((SBFSeri R) * (BSFSeri R)) implies ((SBFSeri R) * (BSFSeri R)) . o = (id (dom (BSFSeri R))) . o )
assume A2:
o in dom ((SBFSeri R) * (BSFSeri R))
;
((SBFSeri R) * (BSFSeri R)) . o = (id (dom (BSFSeri R))) . o
then A3:
o in dom (BSFSeri R)
by FUNCT_2:123;
consider x1 being
Series of 1,
R such that A4:
(
x1 = o &
(BSFSeri R) . o = x1 * NBag1 )
by A2, Def4;
reconsider y =
x1 * NBag1 as
Element of
(Formal-Series R) by FUNCT_2:5, A2, A4;
consider y1 being
sequence of
R such that A5:
(
y1 = y &
(SBFSeri R) . y = y1 * BagN1 )
by Def5;
((SBFSeri R) * (BSFSeri R)) . o =
(SBFSeri R) . (x1 * NBag1)
by A4, A2, FUNCT_2:15
.=
(SBFSeri R) . y
.=
y1 * BagN1
by A5
.=
x1 * (NBag1 * BagN1)
by A5, RELAT_1:36
.=
x1
by Th11, FUNCT_2:17
.=
(id (dom (BSFSeri R))) . o
by A3, A4, FUNCT_1:18
;
hence
((SBFSeri R) * (BSFSeri R)) . o = (id (dom (BSFSeri R))) . o
;
verum
end;
then
(SBFSeri R) * (BSFSeri R) = id (dom (BSFSeri R))
by FUNCT_2:123;
hence
(BSFSeri R) " = SBFSeri R
by A1, FUNCT_1:41; verum