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 & 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 |.h.|) . j = (n -BinarySequence |.i.|) . j

proof

A4: ( |.h.| = h & |.i.| = i ) by A1, ABSVALUE:def 1;
let j be Nat; :: thesis: ( j in Seg n implies (n -BinarySequence |.h.|) . j = (n -BinarySequence |.i.|) . j )
assume A5: j in Seg n ; :: thesis: (n -BinarySequence |.h.|) . j = (n -BinarySequence |.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 |.i.|) = n by CARD_1:def 7;
then A9: (n -BinarySequence |.i.|) . j = (n -BinarySequence |.i.|) /. j by A7, A6, FINSEQ_4:15
.= IFEQ (((|.i.| div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A5, BINARI_3:def 1 ;
len (n -BinarySequence |.h.|) = n by CARD_1:def 7;
then (n -BinarySequence |.h.|) . j = (n -BinarySequence |.h.|) /. j by A7, A6, FINSEQ_4:15
.= IFEQ (((|.h.| div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A5, BINARI_3:def 1
.= IFEQ (((|.i.| div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A2, A8, A4, Lm3 ;
hence (n -BinarySequence |.h.|) . j = (n -BinarySequence |.i.|) . j by A9; :: thesis: verum

end;

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