theorem :: FSCIRC_2:6

for n being Element of NAT
for x, y being FinSeqLen of n
for a, b being set holds
( (n + 1) -BitSubtracterStr ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr (a,b,(n -BitBorrowOutput (x,y)))) & (n + 1) -BitSubtracterCirc ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitSubtracterCirc (x,y)) +* (BitSubtracterWithBorrowCirc (a,b,(n -BitBorrowOutput (x,y)))) & (n + 1) -BitBorrowOutput ((x ^ <*a*>),(y ^ <*b*>)) = BorrowOutput (a,b,(n -BitBorrowOutput (x,y))) )