let R be non degenerated comRing; :: thesis: Polynom-Ring (Polynom-Ring (0,R)), Polynom-Ring (1,R) are_isomorphic
ex P being Function of (Polynom-Ring (Polynom-Ring (0,R))),(Polynom-Ring ((0 + 1),R)) st P is RingIsomorphism by HILBASIS:31;
hence Polynom-Ring (Polynom-Ring (0,R)), Polynom-Ring (1,R) are_isomorphic by QUOFIELD:def 23; :: thesis: verum