:: deftheorem Def2 defines odd_part HURWITZ2:def 2 :
for L being non empty ZeroStr
for p, b₃ being sequence of L holds
( b₃ = odd_part p iff for i being even Nat holds
( b₃ . i = 0. L & ( for i being odd Nat holds b₃ . i = p . i ) ) );