let n be non zero Nat; for z1, z2 being Tuple of n, BOOLEAN st z1,z2 are_summable holds
Absval (z1 + z2) = (Absval z1) + (Absval z2)
let z1, z2 be Tuple of n, BOOLEAN ; ( z1,z2 are_summable implies Absval (z1 + z2) = (Absval z1) + (Absval z2) )
assume
z1,z2 are_summable
; Absval (z1 + z2) = (Absval z1) + (Absval z2)
then
add_ovfl (z1,z2) = FALSE
;
then
IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power n)) = 0
by FUNCOP_1:def 8;
hence Absval (z1 + z2) =
(Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power n)))
.=
(Absval z1) + (Absval z2)
by Th21
;
verum