theorem Th7: :: ALGSEQ_1:16

for i being Nat
for R being non empty ZeroStr holds <%(0. R)%> . i = 0. R