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

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

let j be Nat; :: thesis: ( j in dom (x 'xor' y) implies (x 'xor' y) . j = (y 'xor' x) . j )
assume A4: j in dom (x 'xor' y) ; :: thesis: (x 'xor' y) . j = (y 'xor' x) . j
then A5: j in dom (y 'xor' x) by A3, A2, FINSEQ_1:def 3;
thus (x 'xor' y) . j = (x 'xor' y) /. j by A4, PARTFUN1:def 6
.= (y /. j) 'xor' (x /. j) by A2, A4, Def2
.= (y 'xor' x) /. j by A2, A4, Def2
.= (y 'xor' x) . j by A5, PARTFUN1:def 6 ; :: thesis: verum

end;

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