let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L holds
( p is non-zero iff len p > 0 )
let p be Polynomial of L; :: thesis: ( p is non-zero iff len p > 0 )
hereby :: thesis: ( len p > 0 implies p is non-zero )
assume p is non-zero ; :: thesis: len p > 0
then p <> 0_. L ;
then len p <> 0 by POLYNOM4:5;
hence len p > 0 ; :: thesis: verum
end;
assume len p > 0 ; :: thesis: p is non-zero
then p <> 0_. L by POLYNOM4:3;
hence p is non-zero ; :: thesis: verum