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)%>;

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 )

hence
<%(0. R)%> . i = 0. R
by Def4; :: thesis: verumassume
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;then i > 0 by NAT_1:3;

then i >= len <%(0. R)%> by Th6;

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