let n be non zero Element of NAT ; :: thesis: for s, t being Element of n -tuples_on BOOLEAN holds Op-XOR ((Op-XOR (s,t)),t) = s
let s, t be Element of n -tuples_on BOOLEAN; :: thesis: Op-XOR ((Op-XOR (s,t)),t) = s

now :: thesis: for j being Nat st j in Seg n holds
(Op-XOR ((Op-XOR (s,t)),t)) . j = s . j

let j be Nat; :: thesis: ( j in Seg n implies (Op-XOR ((Op-XOR (s,t)),t)) . j = s . j )
assume A1: j in Seg n ; :: thesis: (Op-XOR ((Op-XOR (s,t)),t)) . j = s . j
thus (Op-XOR ((Op-XOR (s,t)),t)) . j = ((Op-XOR (s,t)) . j) 'xor' (t . j) by A1, Def4
.= ((s . j) 'xor' (t . j)) 'xor' (t . j) by A1, Def4
.= s . j by XBOOLEAN:72 ; :: thesis: verum

end;

hence Op-XOR ((Op-XOR (s,t)),t) = s by FINSEQ_2:119; :: thesis: verum