theorem :: E_TRANS1:12

for f being Element of (Polynom-Ring F_Rat)
for n being non zero Nat st f is irreducible holds
n * f is irreducible