let R be non empty ZeroStr ; :: thesis: for p being AlgSequence of R holds

( p = <%(0. R)%> iff len p = 0 )

let p be AlgSequence of R; :: thesis: ( p = <%(0. R)%> iff len p = 0 )

thus ( p = <%(0. R)%> implies len p = 0 ) by Lm2; :: thesis: ( len p = 0 implies p = <%(0. R)%> )

thus ( len p = 0 implies p = <%(0. R)%> ) :: thesis: verum

( p = <%(0. R)%> iff len p = 0 )

let p be AlgSequence of R; :: thesis: ( p = <%(0. R)%> iff len p = 0 )

thus ( p = <%(0. R)%> implies len p = 0 ) by Lm2; :: thesis: ( len p = 0 implies p = <%(0. R)%> )

thus ( len p = 0 implies p = <%(0. R)%> ) :: thesis: verum