deg (X- a) = 1 by HURWITZ:27;
hence X- a is linear by FIELD_5:def 1; :: thesis: X- a is monic
thus X- a is monic ; :: thesis: verum