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 )

then p <> 0_. L by POLYNOM4:3;

hence p is non-zero ; :: thesis: verum

( 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
len p > 0
; :: thesis: 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;then p <> 0_. L ;

then len p <> 0 by POLYNOM4:5;

hence len p > 0 ; :: thesis: verum

then p <> 0_. L by POLYNOM4:3;

hence p is non-zero ; :: thesis: verum