let L be non trivial right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for p being Element of the carrier of (Polynom-Ring L) holds
( deg p is Element of NAT iff p <> 0. (Polynom-Ring L) )
let p be Element of the carrier of (Polynom-Ring L); :: thesis: ( deg p is Element of NAT iff p <> 0. (Polynom-Ring L) )
set R = Polynom-Ring L;
reconsider pp = p as Polynomial of L ;
A: now :: thesis: ( deg p is Element of NAT implies p <> 0. (Polynom-Ring L) )
assume deg p is Element of NAT ; :: thesis: p <> 0. (Polynom-Ring L)
then p <> 0_. L by HURWITZ:20;
hence p <> 0. (Polynom-Ring L) by POLYNOM3:def 10; :: thesis: verum
end;
now :: thesis: ( p <> 0. (Polynom-Ring L) implies deg p is Element of NAT )
assume p <> 0. (Polynom-Ring L) ; :: thesis: deg p is Element of NAT
then p <> 0_. L by POLYNOM3:def 10;
then len p <> 0 by POLYNOM4:5;
then (len p) + 1 > 0 + 1 by XREAL_1:6;
then len p >= 1 by NAT_1:13;
then (len p) - 1 >= 1 - 1 by XREAL_1:9;
hence deg p is Element of NAT by INT_1:3; :: thesis: verum
end;
hence ( deg p is Element of NAT iff p <> 0. (Polynom-Ring L) ) by A; :: thesis: verum