let n be Element of NAT ; :: thesis: for x being Tuple of n,BOOLEAN holds (ZERO n) 'xor' x = x
let x be Tuple of n,BOOLEAN ; :: thesis: (ZERO n) 'xor' x = x
A1: ( len ((ZERO n) 'xor' x) = n & len x = n ) by FINSEQ_1:def 18;
X: dom ((ZERO n) 'xor' x) = Seg n by A1, FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom ((ZERO n) 'xor' x) implies ((ZERO n) 'xor' x) . j = x . j )
assume A2: j in dom ((ZERO n) 'xor' x) ; :: thesis: ((ZERO n) 'xor' x) . j = x . j
then A3: ( j in dom ((ZERO n) 'xor' x) & j in dom x ) by A1, X, FINSEQ_1:def 3;
j in dom (ZERO n) by A2, X, FUNCOP_1:19;
then A4: (ZERO n) /. j = (n |-> FALSE ) . j by PARTFUN1:def 8
.= FALSE by A2, X, FUNCOP_1:13 ;
thus ((ZERO n) 'xor' x) . j = ((ZERO n) 'xor' x) /. j by A3, PARTFUN1:def 8
.= FALSE 'xor' (x /. j) by A2, A4, Def2, X
.= x /. j by BINARITH:14
.= x . j by A3, PARTFUN1:def 8 ; :: thesis: verum

end;

hence (ZERO n) 'xor' x = x by A1, FINSEQ_2:10; :: thesis: verum