let m be Nat; :: thesis: 2sComplement (m,0) = 0* m
2sComplement (m,0) = m -BinarySequence (abs 0) by Def2
.= m -BinarySequence 0 by ABSVALUE:7 ;
hence 2sComplement (m,0) = 0* m by BINARI_3:26; :: thesis: verum