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

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