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

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

end;

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