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

( 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