let m be non empty Nat; :: thesis: 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 ; :: thesis: 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 ; :: thesis: (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 Th19
.= (z1 ^ <*d1*>) + ((Neg2 z2) ^ <*(('not' d2) 'xor' (add_ovfl ('not' z2),(Bin1 m)))*>) by Th16
.= (z1 + (Neg2 z2)) ^ <*((d1 'xor' (('not' d2) 'xor' (add_ovfl ('not' z2),(Bin1 m)))) 'xor' (add_ovfl z1,(Neg2 z2)))*> by BINARITH:45
.= (z1 + (Neg2 z2)) ^ <*(((d1 'xor' ('not' d2)) 'xor' (add_ovfl ('not' z2),(Bin1 m))) 'xor' (add_ovfl z1,(Neg2 z2)))*> by XBOOLEAN:73 ; :: thesis: verum