let n be non zero 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)
|.i.| = - i by A2, ABSVALUE:def 1;
then 2 to_power (MajP (n,|.i.|)) >= - i by Def1;
then (2 to_power (MajP (n,|.i.|))) + i >= (- i) + i by XREAL_1:6;
then reconsider I = (2 to_power (MajP (n,|.i.|))) + i as Element of NAT by INT_1:3;
|.h.| = - h by A1, ABSVALUE:def 1;
then 2 to_power (MajP (n,|.h.|)) >= - h by Def1;
then (2 to_power (MajP (n,|.h.|))) + h >= (- h) + h by XREAL_1:6;
then reconsider H = (2 to_power (MajP (n,|.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 |.H.|) . j = (n -BinarySequence |.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 |.H.|) . j = (n -BinarySequence |.I.|) . j )
assume A7: j in Seg n ; :: thesis: (n -BinarySequence |.H.|) . j = (n -BinarySequence |.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 & |.H.| = H ) by ABSVALUE:def 1, CARD_1:def 7;
then (n -BinarySequence |.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 |.H.|) . j = (n -BinarySequence |.I.|) . j by ABSVALUE:def 1; :: thesis: verum

end;

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