let i be Nat; :: thesis: for R being non empty ZeroStr holds <%(0. R)%> . i = 0. R
let R be non empty ZeroStr ; :: thesis: <%(0. R)%> . i = 0. R
set p0 = <%(0. R)%>;

now :: thesis: ( i <> 0 implies <%(0. R)%> . i = 0. R )

assume i <> 0 ; :: thesis: <%(0. R)%> . i = 0. R
then i > 0 by NAT_1:3;
then i >= len <%(0. R)%> by Th6;
hence <%(0. R)%> . i = 0. R by Th1; :: thesis: verum

end;

hence <%(0. R)%> . i = 0. R by Def4; :: thesis: verum