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 ;
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 ;
:: thesis: verum