let q be Element of the carrier of (Polynom-Ring F2); :: thesis: ( q = (PolyHom h) . p implies not q is constant )
assume A: q = (PolyHom h) . p ; :: thesis: not q is constant
deg p > 0 by RING_4:def 4;
hence not q is constant by A, FIELD_1:31; :: thesis: verum