let n be Nat; :: thesis: for x, y being FinSequence
for p being set
for f being Function of (2 -tuples_on BOOLEAN ),BOOLEAN holds n -BitGFA0CarryOutput x,y <> [p,f]
let x, y be FinSequence; :: thesis: for p being set
for f being Function of (2 -tuples_on BOOLEAN ),BOOLEAN holds n -BitGFA0CarryOutput x,y <> [p,f]
let p be set ; :: thesis: for f being Function of (2 -tuples_on BOOLEAN ),BOOLEAN holds n -BitGFA0CarryOutput x,y <> [p,f]
let f be Function of (2 -tuples_on BOOLEAN ),BOOLEAN ; :: thesis: n -BitGFA0CarryOutput x,y <> [p,f]
( dom f = 2 -tuples_on BOOLEAN & [p,f] `2 = f ) by FUNCT_2:def 1, MCART_1:7;
then A1: proj1 ([p,f] `2 ) = 2 -tuples_on BOOLEAN ;
( proj1 ((n -BitGFA0CarryOutput x,y) `2 ) = 0 -tuples_on BOOLEAN or proj1 ((n -BitGFA0CarryOutput x,y) `2 ) = 3 -tuples_on BOOLEAN ) by Lm1;
hence n -BitGFA0CarryOutput x,y <> [p,f] by A1, PRALG_1:1; :: thesis: verum