for n being non zero Nat
for z1, z2 being Tuple of n, BOOLEAN st z1,z2 are_summable holds
Absval (z1 + z2) = (Absval z1) + (Absval z2)