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 )
assume p = <%(0. R)%> ; :: thesis: len p = 0
then A1: ( p . 0 = 0. R & len p <= 1 ) by Def4;
0 + 1 = 1 ;
then len p < 1 by A1, Th3, XXREAL_0:1;
hence len p = 0 by NAT_1:14; :: thesis: verum