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
B: deg p > 0 by RING_4:def 4;
deg q = deg p by A, FIELD_1:31;
hence not q is constant by B, RING_4:def 4; :: thesis: verum