let R be non degenerated comRing; :: thesis: (BSPoly R) . (1. (Polynom-Ring (1,R))) = 1. (Polynom-Ring R)
set FS = Formal-Series R;
reconsider PR = Polynom-Ring R as Subring of Formal-Series R by Th35;
A1: 1. PR = 1_. R by POLYNOM3:def 10
.= 1. (Formal-Series R) by POLYALG1:def 2 ;
1. (Formal-Series (1,R)) = 1_ (1,R) by Def3
.= 1. (Polynom-Ring (1,R)) by POLYNOM1:def 11 ;
then (BSPoly R) . (1. (Polynom-Ring (1,R))) = (BSFSeri R) . (1. (Formal-Series (1,R))) by FUNCT_1:49
.= 1. (Polynom-Ring R) by A1, Th30 ;
hence (BSPoly R) . (1. (Polynom-Ring (1,R))) = 1. (Polynom-Ring R) ; :: thesis: verum