let a, b be set ; :: thesis: for c being set st c = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] holds
( 1 -BitGFA0Str <*a*>,<*b*> = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitGFA0Str a,b,c) & 1 -BitGFA0Circ <*a*>,<*b*> = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitGFA0Circ a,b,c) & 1 -BitGFA0CarryOutput <*a*>,<*b*> = GFA0CarryOutput a,b,c )
( <*a*> . 1 = a & <*b*> . 1 = b ) by FINSEQ_1:57;
hence for c being set st c = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] holds
( 1 -BitGFA0Str <*a*>,<*b*> = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitGFA0Str a,b,c) & 1 -BitGFA0Circ <*a*>,<*b*> = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitGFA0Circ a,b,c) & 1 -BitGFA0CarryOutput <*a*>,<*b*> = GFA0CarryOutput a,b,c ) by Th3; :: thesis: verum