let R be non degenerated comRing; :: thesis: ( BSFSeri R is RingIsomorphism & Formal-Series R is Formal-Series (1,R) -isomorphic )
( BSFSeri R is RingHomomorphism & BSFSeri R is isomorphism ) ;
hence ( BSFSeri R is RingIsomorphism & Formal-Series R is Formal-Series (1,R) -isomorphic ) by RING_3:def 4; :: thesis: verum