theorem Th3: :: FSCIRC_2:3

for a, b being FinSequence
for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] holds
( 1 -BitSubtracterStr (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowStr ((a . 1),(b . 1),c)) & 1 -BitSubtracterCirc (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitSubtracterWithBorrowCirc ((a . 1),(b . 1),c)) & 1 -BitBorrowOutput (a,b) = BorrowOutput ((a . 1),(b . 1),c) )