let n be Nat; 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 ; (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 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)) . jlet j be
Nat;
( 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)
;
((x 'xor' y) 'xor' z) . j = (x 'xor' (y 'xor' z)) . jthen 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
;
verum end;
hence
(x 'xor' y) 'xor' z = x 'xor' (y 'xor' z)
by A1, A3, FINSEQ_2:9; verum