let p be non zero Polynomial of (Z/ 2); :: thesis: p is monic
LC p = 1. (Z/ 2) by cz2, TARSKI:def 2;
hence p is monic by RATFUNC1:def 7; :: thesis: verum