let n be 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 by CARD_1:def 7;
then A2: dom (x 'xor' x) = Seg n by FINSEQ_1:def 3;

A3: now :: thesis: for j being Nat st j in dom (x 'xor' x) holds
(x 'xor' x) . j = (ZERO n) . j

let j be Nat; :: thesis: ( j in dom (x 'xor' x) implies (x 'xor' x) . j = (ZERO n) . j )
assume A4: j in dom (x 'xor' x) ; :: thesis: (x 'xor' x) . j = (ZERO n) . j
A5: (ZERO n) . j = FALSE ;
thus (x 'xor' x) . j = (x 'xor' x) /. j by A4, PARTFUN1:def 6
.= (x /. j) 'xor' (x /. j) by A2, A4, Def2
.= (ZERO n) . j by A5, XBOOLEAN:138 ; :: thesis: verum

end;

len (ZERO n) = n by CARD_1:def 7;
hence x 'xor' x = ZERO n by A1, A3, FINSEQ_2:9; :: thesis: verum