let n be non empty Nat; :: thesis: for h, i being Integer st h < 0 & i < 0 & h mod (2 to_power n) = i mod (2 to_power n) holds
2sComplement (n,h) = 2sComplement (n,i)
let h, i be Integer; :: thesis: ( h < 0 & i < 0 & h mod (2 to_power n) = i mod (2 to_power n) implies 2sComplement (n,h) = 2sComplement (n,i) )
assume that
A1: h < 0 and
A2: i < 0 and
A3: h mod (2 to_power n) = i mod (2 to_power n) ; :: thesis: 2sComplement (n,h) = 2sComplement (n,i)
abs i = - i by A2, ABSVALUE:def 1;
then 2 to_power (MajP (n,(abs i))) >= - i by Def1;
then (2 to_power (MajP (n,(abs i)))) + i >= (- i) + i by XREAL_1:6;
then reconsider I = (2 to_power (MajP (n,(abs i)))) + i as Element of NAT by INT_1:3;
abs h = - h by A1, ABSVALUE:def 1;
then 2 to_power (MajP (n,(abs h))) >= - h by Def1;
then (2 to_power (MajP (n,(abs h)))) + h >= (- h) + h by XREAL_1:6;
then reconsider H = (2 to_power (MajP (n,(abs h)))) + h as Element of NAT by INT_1:3;
A4: H mod (2 to_power n) = I mod (2 to_power n) by A3, Lm4;
A5: for j being Nat st j in Seg n holds
(n -BinarySequence (abs H)) . j = (n -BinarySequence (abs I)) . j

proof

A6: len (n -BinarySequence I) = n by CARD_1:def 7;
let j be Nat; :: thesis: ( j in Seg n implies (n -BinarySequence (abs H)) . j = (n -BinarySequence (abs I)) . j )
assume A7: j in Seg n ; :: thesis: (n -BinarySequence (abs H)) . j = (n -BinarySequence (abs I)) . j
A8: 1 <= j by A7, FINSEQ_1:1;
A9: j <= n by A7, FINSEQ_1:1;
reconsider j = j as Nat ;
j - 1 >= 1 - 1 by A8, XREAL_1:9;
then j -' 1 = j - 1 by XREAL_0:def 2;
then A10: j -' 1 < n by A9, XREAL_1:146, XXREAL_0:2;
( len (n -BinarySequence H) = n & abs H = H ) by ABSVALUE:def 1, CARD_1:def 7;
then (n -BinarySequence (abs H)) . j = (n -BinarySequence H) /. j by A8, A9, FINSEQ_4:15
.= IFEQ (((H div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A7, BINARI_3:def 1
.= IFEQ (((I div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A4, A10, Lm3
.= (n -BinarySequence I) /. j by A7, BINARI_3:def 1
.= (n -BinarySequence I) . j by A8, A9, A6, FINSEQ_4:15 ;
hence (n -BinarySequence (abs H)) . j = (n -BinarySequence (abs I)) . j by ABSVALUE:def 1; :: thesis: verum

end;

( 2sComplement (n,h) = n -BinarySequence (abs ((2 to_power (MajP (n,(abs h)))) + h)) & 2sComplement (n,i) = n -BinarySequence (abs ((2 to_power (MajP (n,(abs i)))) + i)) ) by A1, A2, Def2;
hence 2sComplement (n,h) = 2sComplement (n,i) by A5, FINSEQ_2:119; :: thesis: verum