let R be non degenerated comRing; :: thesis: SBFSeri R is onto
rng ((BSFSeri R) * (SBFSeri R)) = rng ((BSFSeri R) * ((BSFSeri R) ")) by Th32
.= rng (BSFSeri R) by FUNCT_1:37
.= the carrier of (Formal-Series R) by FUNCT_2:def 3 ;
hence SBFSeri R is onto by FUNCT_2:22; :: thesis: verum