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

let x be set ; :: thesis: ( dom (('not' (n -BinarySequence 0 )) '&' p) = dom p & ( for x being set 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 set st x in dom (('not' (n -BinarySequence 0 )) '&' p) holds
(('not' (n -BinarySequence 0 )) '&' p) . x = p . x
let x be set ; :: 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:26
.= n |-> 0 by EUCLID:def 4 ;
then (n -BinarySequence 0 ) . x = 0 by A2, A4, FUNCOP_1:13;
then A5: (n -BinarySequence 0 ) /. x = FALSE by A2, A4, A1, PARTFUN1:def 8;
('not' (n -BinarySequence 0 )) /. x = 'not' ((n -BinarySequence 0 ) /. k) by A2, A4, BINARITH:def 4
.= TRUE by A5 ;
hence (('not' (n -BinarySequence 0 )) '&' p) . x = TRUE '&' (p /. x) by A2, A4, Def5
.= p . x by A3, A4, PARTFUN1:def 8 ;
:: thesis: verum

end;

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