theorem Th7: :: FSCIRC_2:7

for n being Nat
for x, y being FinSequence holds
( (n + 1) -BitSubtracterStr (x,y) = (n -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))) & (n + 1) -BitSubtracterCirc (x,y) = (n -BitSubtracterCirc (x,y)) +* (BitSubtracterWithBorrowCirc ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))) & (n + 1) -BitBorrowOutput (x,y) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))) )