theorem Th13: :: NUMERAL2:13

for N, i being Nat st i in dom (Sgm0 (N /\ OddNAT)) holds
(Sgm0 (N /\ OddNAT)) . i = (2 * i) + 1