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