A1: ( SBFSeri R is linear & SBFSeri R is one-to-one ) ;
hence Formal-Series (1,R) is Formal-Series R -homomorphic ; :: thesis: ( Formal-Series (1,R) is Formal-Series R -monomorphic & Formal-Series (1,R) is Formal-Series R -isomorphic )
thus Formal-Series (1,R) is Formal-Series R -monomorphic by A1, RING_3:def 3; :: thesis: Formal-Series (1,R) is Formal-Series R -isomorphic
SBFSeri R is Isomorphism of (Formal-Series R),(Formal-Series (1,R)) ;
hence Formal-Series (1,R) is Formal-Series R -isomorphic by RING_3:def 4; :: thesis: verum