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 (('not' (n -BinarySequence 0 )) '&' p) = Seg n
by Lm1;
hence A2:
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 . xlet x be
set ;
:: thesis: ( x in dom (('not' (n -BinarySequence 0 )) '&' p) implies (('not' (n -BinarySequence 0 )) '&' p) . x = p . x )assume A3:
x in dom (('not' (n -BinarySequence 0 )) '&' p)
;
:: thesis: (('not' (n -BinarySequence 0 )) '&' p) . x = p . xthen reconsider k =
x as
Element of
NAT ;
A4:
n -BinarySequence 0 =
0* n
by BINARI_3:26
.=
n |-> 0
by EUCLID:def 4
;
A5:
dom (n -BinarySequence 0 ) = Seg n
by Lm1;
(n -BinarySequence 0 ) . x = 0
by A1, A3, A4, FUNCOP_1:13;
then A6:
(n -BinarySequence 0 ) /. x = FALSE
by A1, A3, A5, PARTFUN1:def 8;
('not' (n -BinarySequence 0 )) /. x =
'not' ((n -BinarySequence 0 ) /. k)
by A1, A3, BINARITH:def 4
.=
TRUE
by A6
;
hence (('not' (n -BinarySequence 0 )) '&' p) . x =
TRUE '&' (p /. x)
by A1, A3, Def5
.=
p . x
by A2, A3, PARTFUN1:def 8
;
:: thesis: verum end;
hence
('not' (n -BinarySequence 0 )) '&' p = p
by FUNCT_1:9; :: thesis: verum