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

now

let j be Nat; :: thesis: ( j in dom (x 'xor' y) implies (x 'xor' y) . j = (y 'xor' x) . j )
assume A2: j in dom (x 'xor' y) ; :: thesis: (x 'xor' y) . j = (y 'xor' x) . j
then A3: ( j in dom (x 'xor' y) & j in dom (y 'xor' x) ) by A1, X, FINSEQ_1:def 3;
hence (x 'xor' y) . j = (x 'xor' y) /. j by PARTFUN1:def 8
.= (y /. j) 'xor' (x /. j) by A2, Def2, X
.= (y 'xor' x) /. j by A2, Def2, X
.= (y 'xor' x) . j by A3, PARTFUN1:def 8 ;
:: thesis: verum

end;

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