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