let n be non zero Element of NAT ; :: thesis: for u1, v1, w1 being Element of n -tuples_on BOOLEAN holds Op-XOR ((Op-XOR (u1,v1)),w1) = Op-XOR (u1,(Op-XOR (v1,w1)))
let u1, v1, w1 be Element of n -tuples_on BOOLEAN; :: thesis: Op-XOR ((Op-XOR (u1,v1)),w1) = Op-XOR (u1,(Op-XOR (v1,w1)))
A1: len (Op-XOR ((Op-XOR (u1,v1)),w1)) = n by Lm1;
A2: len (Op-XOR (u1,(Op-XOR (v1,w1)))) = n by Lm1;

now :: thesis: for i being Nat st 1 <= i & i <= len (Op-XOR ((Op-XOR (u1,v1)),w1)) holds
(Op-XOR ((Op-XOR (u1,v1)),w1)) . i = (Op-XOR (u1,(Op-XOR (v1,w1)))) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len (Op-XOR ((Op-XOR (u1,v1)),w1)) implies (Op-XOR ((Op-XOR (u1,v1)),w1)) . i = (Op-XOR (u1,(Op-XOR (v1,w1)))) . i )
assume ( 1 <= i & i <= len (Op-XOR ((Op-XOR (u1,v1)),w1)) ) ; :: thesis: (Op-XOR ((Op-XOR (u1,v1)),w1)) . i = (Op-XOR (u1,(Op-XOR (v1,w1)))) . i
then A3: i in Seg n by A1;
thus (Op-XOR ((Op-XOR (u1,v1)),w1)) . i = ((Op-XOR (u1,v1)) . i) 'xor' (w1 . i) by DESCIP_1:def 4, A3
.= ((u1 . i) 'xor' (v1 . i)) 'xor' (w1 . i) by DESCIP_1:def 4, A3
.= (u1 . i) 'xor' ((v1 . i) 'xor' (w1 . i)) by XBOOLEAN:73
.= (u1 . i) 'xor' ((Op-XOR (v1,w1)) . i) by DESCIP_1:def 4, A3
.= (Op-XOR (u1,(Op-XOR (v1,w1)))) . i by DESCIP_1:def 4, A3 ; :: thesis: verum

end;

hence Op-XOR ((Op-XOR (u1,v1)),w1) = Op-XOR (u1,(Op-XOR (v1,w1))) by Lm1, A2, FINSEQ_1:14; :: thesis: verum