theorem :: FSCIRC_2:9

for n being Element of NAT
for x, y being FinSequence holds InnerVertices ((n + 1) -BitSubtracterStr (x,y)) = (InnerVertices (n -BitSubtracterStr (x,y))) \/ (InnerVertices (BitSubtracterWithBorrowStr ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y)))))