let m be non zero Nat; :: thesis: for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds Intval (z ^ <*d*>) = (Absval z) - (IFEQ (d,FALSE,0,(2 to_power m)))
let z be Tuple of m, BOOLEAN ; :: thesis: for d being Element of BOOLEAN holds Intval (z ^ <*d*>) = (Absval z) - (IFEQ (d,FALSE,0,(2 to_power m)))
let d be Element of BOOLEAN ; :: thesis: Intval (z ^ <*d*>) = (Absval z) - (IFEQ (d,FALSE,0,(2 to_power m)))

per cases ( d = FALSE or d = TRUE ) by XBOOLEAN:def 3;

suppose A1: d = FALSE ; :: thesis: Intval (z ^ <*d*>) = (Absval z) - (IFEQ (d,FALSE,0,(2 to_power m)))

then (z ^ <*d*>) /. (m + 1) = FALSE by BINARITH:2;
then A2: Intval (z ^ <*d*>) = Absval (z ^ <*d*>) by Def3
.= (Absval z) + (IFEQ (d,FALSE,0,(2 to_power m))) by BINARITH:20
.= (Absval z) + 0 by A1, FUNCOP_1:def 8
.= Absval z ;
(Absval z) - (IFEQ (d,FALSE,0,(2 to_power m))) = (Absval z) - 0 by A1, FUNCOP_1:def 8
.= Absval z ;
hence Intval (z ^ <*d*>) = (Absval z) - (IFEQ (d,FALSE,0,(2 to_power m))) by A2; :: thesis: verum

end;

suppose A3: d = TRUE ; :: thesis: Intval (z ^ <*d*>) = (Absval z) - (IFEQ (d,FALSE,0,(2 to_power m)))

then (z ^ <*d*>) /. (m + 1) <> FALSE by BINARITH:2;
then Intval (z ^ <*d*>) = (Absval (z ^ <*d*>)) - (2 to_power (m + 1)) by Def3
.= ((Absval z) + (IFEQ (d,FALSE,0,(2 to_power m)))) - (2 to_power (m + 1)) by BINARITH:20
.= ((Absval z) + (2 to_power m)) - (2 to_power (m + 1)) by A3, FUNCOP_1:def 8
.= ((Absval z) + (2 to_power m)) - ((2 to_power m) * (2 to_power 1)) by POWER:27
.= ((Absval z) + (2 to_power m)) - (2 * (2 to_power m)) by POWER:25
.= (Absval z) - (2 to_power m) ;
hence Intval (z ^ <*d*>) = (Absval z) - (IFEQ (d,FALSE,0,(2 to_power m))) by A3, FUNCOP_1:def 8; :: thesis: verum

end;

end;