set x = the Element of L;
take z = [(rpoly (1, the Element of L)),(rpoly (1, the Element of L))]; :: thesis: ( z is reducible & not z is zero )
thus ( z is reducible & not z is zero ) ; :: thesis: verum