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

now

let x be set ; :: thesis: ( dom ((n -BinarySequence 0 ) '&' p) = dom (n -BinarySequence 0 ) & ( for x being set st x in dom ((n -BinarySequence 0 ) '&' p) holds
((n -BinarySequence 0 ) '&' p) . x = (n -BinarySequence 0 ) . x ) )
A1: dom ((n -BinarySequence 0 ) '&' p) = Seg n by Lm1;
hence dom ((n -BinarySequence 0 ) '&' p) = dom (n -BinarySequence 0 ) by Lm1; :: thesis: for x being set st x in dom ((n -BinarySequence 0 ) '&' p) holds
((n -BinarySequence 0 ) '&' p) . x = (n -BinarySequence 0 ) . x
let x be set ; :: thesis: ( x in dom ((n -BinarySequence 0 ) '&' p) implies ((n -BinarySequence 0 ) '&' p) . x = (n -BinarySequence 0 ) . x )
assume A2: x in dom ((n -BinarySequence 0 ) '&' p) ; :: thesis: ((n -BinarySequence 0 ) '&' p) . x = (n -BinarySequence 0 ) . x
A3: dom (n -BinarySequence 0 ) = Seg n by Lm1;
A4: n -BinarySequence 0 = 0* n by BINARI_3:26
.= n |-> 0 by EUCLID:def 4 ;
then (n -BinarySequence 0 ) . x = 0 by A1, A2, FUNCOP_1:13;
then (n -BinarySequence 0 ) /. x = FALSE by A1, A2, A3, PARTFUN1:def 8;
hence ((n -BinarySequence 0 ) '&' p) . x = FALSE '&' (p /. x) by A1, A2, Def5
.= (n -BinarySequence 0 ) . x by A1, A2, A4, FUNCOP_1:13 ;
:: thesis: verum

end;

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