let L be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring L) holds
( p is Unit of (Polynom-Ring L) iff deg p = 0 )
let p be Element of the carrier of (Polynom-Ring L); :: thesis: ( p is Unit of (Polynom-Ring L) iff deg p = 0 )
set R = Polynom-Ring L;
H: 1. (Polynom-Ring L) = 1_. L by POLYNOM3:def 10;

A: now :: thesis: ( p is Unit of (Polynom-Ring L) implies deg p = 0 )

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

end;

now :: thesis: ( deg p = 0 implies p is Unit of (Polynom-Ring L) )

assume AS: deg p = 0 ; :: thesis: p is Unit of (Polynom-Ring L)
then AS1: p <> 0_. L by HURWITZ:20;
p <> 0. (Polynom-Ring L) by AS1, POLYNOM3:def 10;
then reconsider degp = deg p as Nat by T8a;
p is constant by AS;
then consider a being Element of L such that
X: p = a | L by T11;
H3: a <> 0. L by X, AS, HURWITZ:20, UPROOTS:def 5;
set t = (a ") | L;
((a ") | L) *' p = ((a ") * a) | L by X, T4
.= 1_. L by H3, VECTSP_1:def 10 ;
then p divides 1_. L by T2;
hence p is Unit of (Polynom-Ring L) by H, GCD_1:def 20; :: thesis: verum

end;

hence ( p is Unit of (Polynom-Ring L) iff deg p = 0 ) by A; :: thesis: verum