A1: ( BSPoly R is linear & BSPoly R is one-to-one ) ;
hence Polynom-Ring R is Polynom-Ring (1,R) -homomorphic ; :: thesis: ( Polynom-Ring R is Polynom-Ring (1,R) -monomorphic & Polynom-Ring R is Polynom-Ring (1,R) -isomorphic )
thus Polynom-Ring R is Polynom-Ring (1,R) -monomorphic by A1, RING_3:def 3; :: thesis: Polynom-Ring R is Polynom-Ring (1,R) -isomorphic
thus Polynom-Ring R is Polynom-Ring (1,R) -isomorphic by A1, RING_3:def 4; :: thesis: verum