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

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

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

end;

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