theorem Th5: :: FSCIRC_2:5

for n being Nat
for p, q being FinSeqLen of n
for p1, p2, q1, q2 being FinSequence holds
( n -BitSubtracterStr ((p ^ p1),(q ^ q1)) = n -BitSubtracterStr ((p ^ p2),(q ^ q2)) & n -BitSubtracterCirc ((p ^ p1),(q ^ q1)) = n -BitSubtracterCirc ((p ^ p2),(q ^ q2)) & n -BitBorrowOutput ((p ^ p1),(q ^ q1)) = n -BitBorrowOutput ((p ^ p2),(q ^ q2)) )