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

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

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

end;

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