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