take p = 0_. R; :: thesis: ( p is Element of the carrier of (Polynom-Ring R) & p is reducible )
reconsider q = p as Element of (Polynom-Ring R) by POLYNOM3:def 10;
q = 0. (Polynom-Ring R) by POLYNOM3:def 10;
hence ( p is Element of the carrier of (Polynom-Ring R) & p is reducible ) ; :: thesis: verum