let n be non zero Nat; :: thesis: for l, m being Nat st l,m are_congruent_mod 2 to_power n holds
n -BinarySequence l = n -BinarySequence m
let l, m be Nat; :: thesis: ( l,m are_congruent_mod 2 to_power n implies n -BinarySequence l = n -BinarySequence m )
assume l,m are_congruent_mod 2 to_power n ; :: thesis: n -BinarySequence l = n -BinarySequence m
then l mod (2 to_power n) = m mod (2 to_power n) by NAT_D:64;
hence n -BinarySequence l = n -BinarySequence m by Th30; :: thesis: verum