let n be Element of NAT ; :: thesis: for p being Tuple of n, BOOLEAN holds ('not' (n -BinarySequence 0)) '&' p = p
let p be Tuple of n, BOOLEAN ; :: thesis: ('not' (n -BinarySequence 0)) '&' p = p
set B = n -BinarySequence 0;
set nB = 'not' (n -BinarySequence 0);

now :: thesis: for x being set holds
( dom (('not' (n -BinarySequence 0)) '&' p) = dom p & ( for x being object st x in dom (('not' (n -BinarySequence 0)) '&' p) holds
(('not' (n -BinarySequence 0)) '&' p) . x = p . x ) )

let x be set ; :: thesis: ( dom (('not' (n -BinarySequence 0)) '&' p) = dom p & ( for x being object st x in dom (('not' (n -BinarySequence 0)) '&' p) holds
(('not' (n -BinarySequence 0)) '&' p) . x = p . x ) )
A1: dom (n -BinarySequence 0) = Seg n by Lm1;
A2: dom (('not' (n -BinarySequence 0)) '&' p) = Seg n by Lm1;
hence A3: dom (('not' (n -BinarySequence 0)) '&' p) = dom p by Lm1; :: thesis: for x being object st x in dom (('not' (n -BinarySequence 0)) '&' p) holds
(('not' (n -BinarySequence 0)) '&' p) . x = p . x
let x be object ; :: thesis: ( x in dom (('not' (n -BinarySequence 0)) '&' p) implies (('not' (n -BinarySequence 0)) '&' p) . x = p . x )
assume A4: x in dom (('not' (n -BinarySequence 0)) '&' p) ; :: thesis: (('not' (n -BinarySequence 0)) '&' p) . x = p . x
then reconsider k = x as Element of NAT ;
n -BinarySequence 0 = 0* n by BINARI_3:25
.= n |-> 0 by EUCLID:def 4 ;
then (n -BinarySequence 0) . x = 0 ;
then A5: (n -BinarySequence 0) /. x = FALSE by A2, A4, A1, PARTFUN1:def 6;
('not' (n -BinarySequence 0)) /. x = 'not' ((n -BinarySequence 0) /. k) by A2, A4, BINARITH:def 1
.= TRUE by A5 ;
hence (('not' (n -BinarySequence 0)) '&' p) . x = TRUE '&' (p /. x) by A2, A4, Def5
.= p . x by A3, A4, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence ('not' (n -BinarySequence 0)) '&' p = p by FUNCT_1:2; :: thesis: verum