theorem ZZ2: :: FIELD_14:39
for F being Field
for p, q being Polynomial of F
for r being monic Polynomial of F holds (r *' p) gcd (r *' q) = r *' (p gcd q)