let m be non empty Nat; :: thesis: for x, y being Tuple of m,BOOLEAN holds x - y = x + (Neg2 y)
let x, y be Tuple of m,BOOLEAN ; :: thesis: x - y = x + (Neg2 y)
for i being Nat st i in Seg m holds
(x - y) /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i) by Def6;
hence x - y = x + (Neg2 y) by BINARITH:def 8; :: thesis: verum