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

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

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

end;

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