let L be domRing; :: thesis: for p being Element of the carrier of (Polynom-Ring L) st p is Unit of (Polynom-Ring L) holds
deg p = 0
let p be Element of the carrier of (Polynom-Ring L); :: thesis: ( p is Unit of (Polynom-Ring L) implies deg p = 0 )
set R = Polynom-Ring L;
H: 1. (Polynom-Ring L) = 1_. L by POLYNOM3:def 10;
assume AS: p is Unit of (Polynom-Ring L) ; :: thesis: deg p = 0
then H0: p <> 0. (Polynom-Ring L) ;
then H1: p <> 0_. L by POLYNOM3:def 10;
reconsider degp = deg p as Element of NAT by H0, T8a;
p divides 1_. L by AS, H, GCD_1:def 20;
then consider t being Polynomial of L such that
H3: p *' t = 1_. L by T2;
reconsider t = t as Element of the carrier of (Polynom-Ring L) by POLYNOM3:def 10;
H5: t <> 0_. L by POLYNOM3:34, H3;
then t <> 0. (Polynom-Ring L) by POLYNOM3:def 10;
then reconsider degt = deg t as Element of NAT by T8a;
degt + degp = deg (1_. L) by H1, H3, H5, HURWITZ:23
.= 1 - 1 by POLYNOM4:4 ;
hence deg p = 0 ; :: thesis: verum