theorem Th2: :: GFACIRC2:2

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