let n be Element of NAT ; :: thesis: for p being Element of n -tuples_on BOOLEAN holds (n -BinarySequence 0) '&' p = n -BinarySequence 0
let p be Element of n -tuples_on BOOLEAN; :: thesis: (n -BinarySequence 0) '&' p = n -BinarySequence 0
set B = n -BinarySequence 0;
now :: thesis: for x being object holds
( dom ((n -BinarySequence 0) '&' p) = dom (n -BinarySequence 0) & ( for x being object st x in dom ((n -BinarySequence 0) '&' p) holds
((n -BinarySequence 0) '&' p) . x = (n -BinarySequence 0) . x ) )
let x be object ; :: thesis: ( dom ((n -BinarySequence 0) '&' p) = dom (n -BinarySequence 0) & ( for x being object st x in dom ((n -BinarySequence 0) '&' p) holds
((n -BinarySequence 0) '&' p) . x = (n -BinarySequence 0) . x ) )
A1: dom (n -BinarySequence 0) = Seg n by Lm1;
A2: 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 object st x in dom ((n -BinarySequence 0) '&' p) holds
((n -BinarySequence 0) '&' p) . x = (n -BinarySequence 0) . x
let x be object ; :: thesis: ( x in dom ((n -BinarySequence 0) '&' p) implies ((n -BinarySequence 0) '&' p) . x = (n -BinarySequence 0) . x )
assume A3: x in dom ((n -BinarySequence 0) '&' p) ; :: thesis: ((n -BinarySequence 0) '&' p) . x = (n -BinarySequence 0) . x
A4: n -BinarySequence 0 = 0* n by BINARI_3:25
.= n |-> 0 by EUCLID:def 4 ;
then (n -BinarySequence 0) . x = 0 ;
then (n -BinarySequence 0) /. x = FALSE by A2, A3, A1, PARTFUN1:def 6;
hence ((n -BinarySequence 0) '&' p) . x = FALSE '&' (p /. x) by A2, A3, Def5
.= (n -BinarySequence 0) . x by A4 ;
:: thesis: verum
end;
hence (n -BinarySequence 0) '&' p = n -BinarySequence 0 by FUNCT_1:2; :: thesis: verum