let n be non zero Nat; for h, i being Integer st ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & h,i are_congruent_mod 2 to_power n holds
2sComplement (n,h) = 2sComplement (n,i)
let h, i be Integer; ( ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & h,i are_congruent_mod 2 to_power n implies 2sComplement (n,h) = 2sComplement (n,i) )
assume that
A1:
( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) )
and
A2:
h,i are_congruent_mod 2 to_power n
; 2sComplement (n,h) = 2sComplement (n,i)
h mod (2 to_power n) = i mod (2 to_power n)
by A2, NAT_D:64;
hence
2sComplement (n,h) = 2sComplement (n,i)
by A1, Lm5, Lm6; verum