let l, m be Nat; :: thesis: ex x being Element of BOOLEAN st (m + 1) -BinarySequence l = (m -BinarySequence l) ^ <*x*>
consider x being Element of BOOLEAN such that
A1: 2sComplement ((m + 1),l) = (2sComplement (m,l)) ^ <*x*> by Th33;
A2: |.l.| = l by ABSVALUE:def 1;
then (m + 1) -BinarySequence l = (2sComplement (m,l)) ^ <*x*> by A1, Def2
.= (m -BinarySequence l) ^ <*x*> by A2, Def2 ;
hence ex x being Element of BOOLEAN st (m + 1) -BinarySequence l = (m -BinarySequence l) ^ <*x*> ; :: thesis: verum