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