let m, l 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: abs 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