let m be non zero 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 5; :: thesis: verum