let n be non zero Nat; :: thesis: for x being Tuple of n, BOOLEAN holds n -BinarySequence (Absval x) = x
let x be Tuple of n, BOOLEAN ; :: thesis: n -BinarySequence (Absval x) = x
Absval x < 2 to_power n by Th1;
then Absval (n -BinarySequence (Absval x)) = Absval x by Th35;
hence n -BinarySequence (Absval x) = x by Th2; :: thesis: verum