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

proof

assume len p = 0 ; :: thesis: p = <%(0. R)%>
then ( len p = len <%(0. R)%> & ( for k being Nat st k < len p holds
p . k = <%(0. R)%> . k ) ) by Lm2, NAT_1:2;
hence p = <%(0. R)%> by Th4; :: thesis: verum

end;