let n be Nat; :: thesis: for x, y, z being Tuple of n, BOOLEAN holds (x 'xor' y) 'xor' z = x 'xor' (y 'xor' z)
let x, y, z be Tuple of n, BOOLEAN ; :: thesis: (x 'xor' y) 'xor' z = x 'xor' (y 'xor' z)
A1: len ((x 'xor' y) 'xor' z) = n by CARD_1:def 7;
then A2: dom ((x 'xor' y) 'xor' z) = Seg n by FINSEQ_1:def 3;
A3: len (x 'xor' (y 'xor' z)) = n by CARD_1:def 7;

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

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

end;

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