let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for p being Element of the carrier of (Polynom-Ring L) holds
( ( not p is zero & p is constant ) iff deg p = 0 )
let p be Element of the carrier of (Polynom-Ring L); :: thesis: ( ( not p is zero & p is constant ) iff deg p = 0 )
A: now :: thesis: ( not p is zero & p is constant implies deg p = 0 )
assume AS: ( not p is zero & p is constant ) ; :: thesis: deg p = 0
now :: thesis: not deg p <> 0
assume deg p <> 0 ; :: thesis: contradiction
then ((len p) - 1) + 1 < 0 + 1 by AS, XREAL_1:6;
then len p = 0 by NAT_1:14;
then deg p = - 1 ;
then p = 0_. L by HURWITZ:20;
hence contradiction by AS; :: thesis: verum
end;
hence deg p = 0 ; :: thesis: verum
end;
now :: thesis: ( deg p = 0 implies ( not p is zero & p is constant ) )
assume AS: deg p = 0 ; :: thesis: ( not p is zero & p is constant )
then p <> 0_. L by HURWITZ:20;
hence not p is zero by UPROOTS:def 5; :: thesis: p is constant
thus p is constant by AS; :: thesis: verum
end;
hence ( ( not p is zero & p is constant ) iff deg p = 0 ) by A; :: thesis: verum