let n be non zero Nat; :: thesis: 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 ; :: thesis: ( z1,z2 are_summable implies Absval (z1 + z2) = (Absval z1) + (Absval z2) )
assume z1,z2 are_summable ; :: thesis: Absval (z1 + z2) = (Absval z1) + (Absval z2)
then add_ovfl z1,z2 = FALSE by Def10;
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 Th47 ;
:: thesis: verum