let n be Element of NAT ; :: thesis: for x, y being FinSequence
for p being set holds
( n -BitBorrowOutput x,y <> [p,and2 ] & n -BitBorrowOutput x,y <> [p,and2a ] & n -BitBorrowOutput x,y <> [p,'xor' ] )
let x, y be FinSequence; :: thesis: for p being set holds
( n -BitBorrowOutput x,y <> [p,and2 ] & n -BitBorrowOutput x,y <> [p,and2a ] & n -BitBorrowOutput x,y <> [p,'xor' ] )
let p be set ; :: thesis: ( n -BitBorrowOutput x,y <> [p,and2 ] & n -BitBorrowOutput x,y <> [p,and2a ] & n -BitBorrowOutput x,y <> [p,'xor' ] )
A1: dom and2 = 2 -tuples_on BOOLEAN by FUNCT_2:def 1;
A2: dom and2a = 2 -tuples_on BOOLEAN by FUNCT_2:def 1;
A3: dom 'xor' = 2 -tuples_on BOOLEAN by FUNCT_2:def 1;
A4: proj1 ([p,and2 ] `2 ) = 2 -tuples_on BOOLEAN by A1, MCART_1:7;
A5: proj1 ([p,and2a ] `2 ) = 2 -tuples_on BOOLEAN by A2, MCART_1:7;
A6: proj1 ([p,'xor' ] `2 ) = 2 -tuples_on BOOLEAN by A3, MCART_1:7;
( proj1 ((n -BitBorrowOutput x,y) `2 ) = 0 -tuples_on BOOLEAN or proj1 ((n -BitBorrowOutput x,y) `2 ) = 3 -tuples_on BOOLEAN ) by Th18;
hence ( n -BitBorrowOutput x,y <> [p,and2 ] & n -BitBorrowOutput x,y <> [p,and2a ] & n -BitBorrowOutput x,y <> [p,'xor' ] ) by A4, A5, A6, FINSEQ_2:130; :: thesis: verum