let n be non empty Nat; :: thesis: for l, m being Nat st l mod (2 to_power n) = m mod (2 to_power n) holds
n -BinarySequence l = n -BinarySequence m
let l, m be Nat; :: thesis: ( l mod (2 to_power n) = m mod (2 to_power n) implies n -BinarySequence l = n -BinarySequence m )
assume A1: l mod (2 to_power n) = m mod (2 to_power n) ; :: thesis: n -BinarySequence l = n -BinarySequence m
( abs l = l & abs m = m ) by ABSVALUE:def 1;
then ( 2sComplement n,l = n -BinarySequence l & 2sComplement n,m = n -BinarySequence m ) by Def2;
hence n -BinarySequence l = n -BinarySequence m by A1, Lm5; :: thesis: verum