theorem :: E_TRANS1:14

for g being Polynomial of F_Rat st deg g >= 2 & @ g is irreducible holds
g . 0 <> 0. F_Rat