let R be non degenerated comRing; :: thesis: (BSFSeri R) . (1. (Formal-Series (1,R))) = 1. (Formal-Series R)
consider e1 being Series of 1,R such that
A1: ( e1 = 1. (Formal-Series (1,R)) & (BSFSeri R) . (1. (Formal-Series (1,R))) = e1 * NBag1 ) by Def4;
e1 = 1_ (1,R) by A1, Def3;
then (BSFSeri R) . (1. (Formal-Series (1,R))) = ((0_ (1,R)) +* ((EmptyBag 1),(1. R))) * NBag1 by A1
.= 1_. R by Th23
.= 1. (Formal-Series R) by POLYALG1:def 2 ;
hence (BSFSeri R) . (1. (Formal-Series (1,R))) = 1. (Formal-Series R) ; :: thesis: verum