let u be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: for a, b being Element of INT.Ring holds eval ((a * (~ u)),b) in {a} -Ideal
let a, b be Element of INT.Ring; :: thesis: eval ((a * (~ u)),b) in {a} -Ideal
eval ((a * (~ u)),b) = a * (eval ((~ u),b)) by RING_5:7;
hence eval ((a * (~ u)),b) in {a} -Ideal by RING_2:18, GCD_1:def 1; :: thesis: verum