theorem Th3: :: GFACIRC2:3

for a, b being FinSequence
for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] holds
( 1 -BitGFA0Str (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (BitGFA0Str ((a . 1),(b . 1),c)) & 1 -BitGFA0Circ (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (BitGFA0Circ ((a . 1),(b . 1),c)) & 1 -BitGFA0CarryOutput (a,b) = GFA0CarryOutput ((a . 1),(b . 1),c) )