for n being non zero Nat
for x being Tuple of n, BOOLEAN
for m, l being Nat
for y being Tuple of l, BOOLEAN st y = x ^ (0* m) holds
Absval y = Absval x