let a, b be set ; :: thesis: for c being set st c = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] holds
( 1 -BitGFA1Str <*a*>,<*b*> = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitGFA1Str a,b,c) & 1 -BitGFA1Circ <*a*>,<*b*> = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitGFA1Circ a,b,c) & 1 -BitGFA1CarryOutput <*a*>,<*b*> = GFA1CarryOutput a,b,c )
( <*a*> . 1 = a & <*b*> . 1 = b ) by FINSEQ_1:57;
hence for c being set st c = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] holds
( 1 -BitGFA1Str <*a*>,<*b*> = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitGFA1Str a,b,c) & 1 -BitGFA1Circ <*a*>,<*b*> = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitGFA1Circ a,b,c) & 1 -BitGFA1CarryOutput <*a*>,<*b*> = GFA1CarryOutput a,b,c ) by Th17; :: thesis: verum