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