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:1;
A7: 1 <= j by A5, FINSEQ_1:1;
then j - 1 >= 1 - 1 by XREAL_1:9;
then j -' 1 = j - 1 by XREAL_0:def 2;
then A8: j -' 1 < n by A6, XREAL_1:146, XXREAL_0:2;
len (n -BinarySequence (abs i)) = n by CARD_1:def 7;
then A9: (n -BinarySequence (abs i)) . j = (n -BinarySequence (abs i)) /. j by A7, A6, FINSEQ_4:15
.= 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 CARD_1:def 7;
then (n -BinarySequence (abs h)) . j = (n -BinarySequence (abs h)) /. j by A7, A6, FINSEQ_4:15
.= 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:119; :: thesis: verum