take 0. (Polynom-Ring R) ; :: thesis: 0. (Polynom-Ring R) is zero
thus 0. (Polynom-Ring R) is zero ; :: thesis: verum