let L be non empty ZeroStr ; :: thesis: for p being AlgSequence of L st len p = 1 holds
( p = <%(p . 0)%> & p . 0 <> 0. L )
let p be AlgSequence of L; :: thesis: ( len p = 1 implies ( p = <%(p . 0)%> & p . 0 <> 0. L ) )
assume A1: len p = 1 ; :: thesis: ( p = <%(p . 0)%> & p . 0 <> 0. L )
thus p = <%(p . 0)%> by A1, ALGSEQ_1:def 5; :: thesis: p . 0 <> 0. L
hence p . 0 <> 0. L by A1, ALGSEQ_1:14; :: thesis: verum