let R be non empty ZeroStr ; :: thesis: for p being AlgSequence of R st p = <%(0. R)%> holds
len p = 0
let p be AlgSequence of R; :: thesis: ( p = <%(0. R)%> implies len p = 0 )
A1: 0 + 1 = 1 ;
assume p = <%(0. R)%> ; :: thesis: len p = 0
then ( len p <= 1 & p . 0 = 0. R ) by Def6;
then ( len p <= 1 & len p <> 1 ) by A1, Th25;
then len p < 1 by XXREAL_0:1;
hence len p = 0 by NAT_1:14; :: thesis: verum