theorem Th19: :: BINARI_3:19

for n being non zero Nat
for x, y being Tuple of n, BOOLEAN st x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds
for k being non zero Nat st k <> 1 & k <= n holds
( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )