let R be non degenerated comRing; :: thesis: ( BSPoly R is RingIsomorphism & Polynom-Ring R is Polynom-Ring (1,R) -isomorphic )
( BSPoly R is RingHomomorphism & BSPoly R is isomorphism ) ;
hence ( BSPoly R is RingIsomorphism & Polynom-Ring R is Polynom-Ring (1,R) -isomorphic ) by RING_3:def 4; :: thesis: verum