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