let m be non zero Nat; for z1, z2 being Tuple of m, BOOLEAN
for d1, d2 being Element of BOOLEAN holds (z1 ^ <*d1*>) - (z2 ^ <*d2*>) = (z1 + (Neg2 z2)) ^ <*(((d1 'xor' ('not' d2)) 'xor' (add_ovfl (('not' z2),(Bin1 m)))) 'xor' (add_ovfl (z1,(Neg2 z2))))*>
let z1, z2 be Tuple of m, BOOLEAN ; for d1, d2 being Element of BOOLEAN holds (z1 ^ <*d1*>) - (z2 ^ <*d2*>) = (z1 + (Neg2 z2)) ^ <*(((d1 'xor' ('not' d2)) 'xor' (add_ovfl (('not' z2),(Bin1 m)))) 'xor' (add_ovfl (z1,(Neg2 z2))))*>
let d1, d2 be Element of BOOLEAN ; (z1 ^ <*d1*>) - (z2 ^ <*d2*>) = (z1 + (Neg2 z2)) ^ <*(((d1 'xor' ('not' d2)) 'xor' (add_ovfl (('not' z2),(Bin1 m)))) 'xor' (add_ovfl (z1,(Neg2 z2))))*>
thus (z1 ^ <*d1*>) - (z2 ^ <*d2*>) =
(z1 ^ <*d1*>) + (Neg2 (z2 ^ <*d2*>))
by Th17
.=
(z1 ^ <*d1*>) + ((Neg2 z2) ^ <*(('not' d2) 'xor' (add_ovfl (('not' z2),(Bin1 m))))*>)
by Th14
.=
(z1 + (Neg2 z2)) ^ <*((d1 'xor' (('not' d2) 'xor' (add_ovfl (('not' z2),(Bin1 m))))) 'xor' (add_ovfl (z1,(Neg2 z2))))*>
by BINARITH:19
.=
(z1 + (Neg2 z2)) ^ <*(((d1 'xor' ('not' d2)) 'xor' (add_ovfl (('not' z2),(Bin1 m)))) 'xor' (add_ovfl (z1,(Neg2 z2))))*>
by XBOOLEAN:73
; verum