let R be domRing; :: thesis: for p, q being Element of the carrier of (Polynom-Ring R) st p is_associated_to q holds
deg p = deg q
let p, q be Element of the carrier of (Polynom-Ring R); :: thesis: ( p is_associated_to q implies deg p = deg q )
assume A: p is_associated_to q ; :: thesis: deg p = deg q
then consider c being Element of (Polynom-Ring R) such that
K2: q = p * c by GCD_1:def 1;
reconsider r = c as Element of the carrier of (Polynom-Ring R) ;
consider d being Element of (Polynom-Ring R) such that
K3: p = q * d by A, GCD_1:def 1;
reconsider s = d as Element of the carrier of (Polynom-Ring R) ;
K4: q = p *' r by K2, POLYNOM3:def 10;
K5: p = q *' s by K3, POLYNOM3:def 10;