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