let R be non degenerated comRing; :: thesis: ( BSFSeri R is one-to-one & BSFSeri R is onto )
A1: for x1, x2 being object st x1 in dom (BSFSeri R) & x2 in dom (BSFSeri R) & (BSFSeri R) . x1 = (BSFSeri R) . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom (BSFSeri R) & x2 in dom (BSFSeri R) & (BSFSeri R) . x1 = (BSFSeri R) . x2 implies x1 = x2 )
assume A2: ( x1 in dom (BSFSeri R) & x2 in dom (BSFSeri R) & (BSFSeri R) . x1 = (BSFSeri R) . x2 ) ; :: thesis: x1 = x2
then consider xx1 being Series of 1,R such that
A3: ( xx1 = x1 & (BSFSeri R) . x1 = xx1 * NBag1 ) by Def4;
consider xx2 being Series of 1,R such that
A4: ( xx2 = x2 & (BSFSeri R) . x2 = xx2 * NBag1 ) by A2, Def4;
A5: for o being object st o in Bags 1 holds
xx1 . o = xx2 . o

proof

let o be object ; :: thesis: ( o in Bags 1 implies xx1 . o = xx2 . o )
assume o in Bags 1 ; :: thesis: xx1 . o = xx2 . o
then reconsider b = o as Element of Bags 1 ;
A6: b = 1 --> (b . 0) by Th5
.= NBag1 . (b . 0) by Def1 ;
xx1 . o = (xx2 * NBag1) . (b . 0) by A3, A4, A2, A6, FUNCT_2:15
.= xx2 . o by A6, FUNCT_2:15 ;
hence xx1 . o = xx2 . o ; :: thesis: verum

end;

x1 = xx1 by A3
.= xx2 by A5
.= x2 by A4 ;
hence x1 = x2 ; :: thesis: verum

end;

rng (BSFSeri R) = the carrier of (Formal-Series R)

proof

for o being object st o in the carrier of (Formal-Series R) holds
ex x being object st
( x in the carrier of (Formal-Series (1,R)) & o = (BSFSeri R) . x )

proof

let o be object ; :: thesis: ( o in the carrier of (Formal-Series R) implies ex x being object st
( x in the carrier of (Formal-Series (1,R)) & o = (BSFSeri R) . x ) )
assume o in the carrier of (Formal-Series R) ; :: thesis: ex x being object st
( x in the carrier of (Formal-Series (1,R)) & o = (BSFSeri R) . x )
then reconsider s = o as sequence of R by POLYALG1:def 2;
s * BagN1 in the carrier of (Formal-Series (1,R)) by Def3;
then consider x being object such that
A7: ( x in the carrier of (Formal-Series (1,R)) & x = s * BagN1 ) ;
consider x1 being Series of 1,R such that
A8: ( x1 = x & (BSFSeri R) . x = x1 * NBag1 ) by A7, Def4;
(BSFSeri R) . x = s * (BagN1 * NBag1) by A7, A8, RELAT_1:36
.= o by FUNCT_2:17, Th10 ;
hence ex x being object st
( x in the carrier of (Formal-Series (1,R)) & o = (BSFSeri R) . x ) by A7; :: thesis: verum

end;

hence rng (BSFSeri R) = the carrier of (Formal-Series R) by FUNCT_2:10; :: thesis: verum

end;

hence ( BSFSeri R is one-to-one & BSFSeri R is onto ) by A1; :: thesis: verum