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

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