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 & i >= 0 ) and
A2: h mod (2 to_power n) = i mod (2 to_power n) ; :: thesis: 2sComplement n,h = 2sComplement n,i
A3: for j being Nat st j in Seg n holds
(n -BinarySequence (abs h)) . j = (n -BinarySequence (abs i)) . j

proof

A4: ( abs h = h & abs i = i ) by A1, ABSVALUE:def 1;
let j be Nat; :: thesis: ( j in Seg n implies (n -BinarySequence (abs h)) . j = (n -BinarySequence (abs i)) . j )
assume A5: j in Seg n ; :: thesis: (n -BinarySequence (abs h)) . j = (n -BinarySequence (abs i)) . j
reconsider j = j as Nat ;
A6: j <= n by A5, FINSEQ_1:3;
A7: 1 <= j by A5, FINSEQ_1:3;
then j - 1 >= 1 - 1 by XREAL_1:11;
then j -' 1 = j - 1 by XREAL_0:def 2;
then A8: j -' 1 < n by A6, XREAL_1:148, XXREAL_0:2;
len (n -BinarySequence (abs i)) = n by FINSEQ_1:def 18;
then A9: (n -BinarySequence (abs i)) . j = (n -BinarySequence (abs i)) /. j by A7, A6, FINSEQ_4:24
.= IFEQ (((abs i) div (2 to_power (j -' 1))) mod 2),0 ,FALSE ,TRUE by A5, BINARI_3:def 1 ;
len (n -BinarySequence (abs h)) = n by FINSEQ_1:def 18;
then (n -BinarySequence (abs h)) . j = (n -BinarySequence (abs h)) /. j by A7, A6, FINSEQ_4:24
.= IFEQ (((abs h) div (2 to_power (j -' 1))) mod 2),0 ,FALSE ,TRUE by A5, BINARI_3:def 1
.= IFEQ (((abs i) div (2 to_power (j -' 1))) mod 2),0 ,FALSE ,TRUE by A2, A8, A4, Lm3 ;
hence (n -BinarySequence (abs h)) . j = (n -BinarySequence (abs i)) . j by A9; :: thesis: verum

end;

( 2sComplement n,h = n -BinarySequence (abs h) & 2sComplement n,i = n -BinarySequence (abs i) ) by A1, Def2;
hence 2sComplement n,h = 2sComplement n,i by A3, FINSEQ_2:139; :: thesis: verum