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

now

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

end;

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