let m be non empty Nat; :: thesis: for z1, z2 being Tuple of m,BOOLEAN
for d1, d2 being Element of BOOLEAN holds Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>)) = (((Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))) - (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) + (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))
let z1, z2 be Tuple of m,BOOLEAN ; :: thesis: for d1, d2 being Element of BOOLEAN holds Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>)) = (((Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))) - (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) + (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))
let d1, d2 be Element of BOOLEAN ; :: thesis: Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>)) = (((Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))) - (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) + (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))
set A = Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>));
set B = IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1));
set C = IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1));
set D = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>));
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>)) by Th13;
hence Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>)) = (((Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))) - (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) + (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) ; :: thesis: verum