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;

per cases ( p = 0_. R or q = 0_. R or ( p <> 0_. R & q <> 0_. R ) ) ;

suppose p = 0_. R ; :: thesis: deg p = deg q

hence deg p = deg q by K4, POLYNOM3:34; :: thesis: verum

end;

suppose q = 0_. R ; :: thesis: deg p = deg q

hence deg p = deg q by K5, POLYNOM3:34; :: thesis: verum

end;

suppose A: ( p <> 0_. R & q <> 0_. R ) ; :: thesis: deg p = deg q

then A1: ( r <> 0_. R & s <> 0_. R ) by K4, K5, POLYNOM3:34;
then A2: ( deg r is Element of NAT & deg s is Element of NAT ) by T8b;
A3: ( deg q = (deg p) + (deg r) & deg p = (deg q) + (deg s) ) by A, A1, K4, K5, HURWITZ:23;
then (deg r) + (deg s) = 0 ;
then ( deg r = 0 & deg s = 0 ) by A2;
hence deg p = deg q by A3; :: thesis: verum

end;

end;