theorem Th29: :: POLYALGX:29

for R being non degenerated comRing
for f, g being Element of (Formal-Series (1,R)) holds (BSFSeri R) . (f * g) = ((BSFSeri R) . f) * ((BSFSeri R) . g)