let n be Nat; for x, y being FinSequence
for p being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds n -BitGFA1CarryOutput (x,y) <> [p,f]
let x, y be FinSequence; for p being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds n -BitGFA1CarryOutput (x,y) <> [p,f]
let p be set ; for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds n -BitGFA1CarryOutput (x,y) <> [p,f]
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; n -BitGFA1CarryOutput (x,y) <> [p,f]
dom f = 2 -tuples_on BOOLEAN
by FUNCT_2:def 1;
then A1:
proj1 ([p,f] `2) = 2 -tuples_on BOOLEAN
;
( proj1 ((n -BitGFA1CarryOutput (x,y)) `2) = 0 -tuples_on BOOLEAN or proj1 ((n -BitGFA1CarryOutput (x,y)) `2) = 3 -tuples_on BOOLEAN )
by Lm3;
hence
n -BitGFA1CarryOutput (x,y) <> [p,f]
by A1, FINSEQ_2:110; verum