theorem Th16: :: GFACIRC2:16

for a, b being FinSequence holds
( 0 -BitGFA1Str (a,b) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & 0 -BitGFA1Circ (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & 0 -BitGFA1CarryOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] )