let n be non zero Nat; :: thesis: for z being Tuple of n, BOOLEAN
for d being Element of BOOLEAN holds Absval (z ^ <*d*>) = (Absval z) + (IFEQ d,FALSE ,0 ,(2 to_power n))
let z be Tuple of n, BOOLEAN ; :: thesis: for d being Element of BOOLEAN holds Absval (z ^ <*d*>) = (Absval z) + (IFEQ d,FALSE ,0 ,(2 to_power n))
let d be Element of BOOLEAN ; :: thesis: Absval (z ^ <*d*>) = (Absval z) + (IFEQ d,FALSE ,0 ,(2 to_power n))
for i being Nat st i in Seg (n + 1) holds
((Binary z) ^ <*(IFEQ d,FALSE ,0 ,(2 to_power n))*>) /. i = IFEQ ((z ^ <*d*>) /. i),FALSE ,0 ,(2 to_power (i -' 1))

proof

A1: Seg (n + 1) = (Seg n) \/ {.(n + 1).} by FINSEQ_1:11;
let i be Nat; :: thesis: ( i in Seg (n + 1) implies ((Binary z) ^ <*(IFEQ d,FALSE ,0 ,(2 to_power n))*>) /. i = IFEQ ((z ^ <*d*>) /. i),FALSE ,0 ,(2 to_power (i -' 1)) )
assume A2: i in Seg (n + 1) ; :: thesis: ((Binary z) ^ <*(IFEQ d,FALSE ,0 ,(2 to_power n))*>) /. i = IFEQ ((z ^ <*d*>) /. i),FALSE ,0 ,(2 to_power (i -' 1))

per cases ( i in Seg n or i in {.(n + 1).} ) by A2, A1, XBOOLE_0:def 3;

suppose A3: i in Seg n ; :: thesis: ((Binary z) ^ <*(IFEQ d,FALSE ,0 ,(2 to_power n))*>) /. i = IFEQ ((z ^ <*d*>) /. i),FALSE ,0 ,(2 to_power (i -' 1))

hence ((Binary z) ^ <*(IFEQ d,FALSE ,0 ,(2 to_power n))*>) /. i = (Binary z) /. i by Th2
.= IFEQ (z /. i),FALSE ,0 ,(2 to_power (i -' 1)) by A3, Def6
.= IFEQ ((z ^ <*d*>) /. i),FALSE ,0 ,(2 to_power (i -' 1)) by A3, Th2 ;
:: thesis: verum

end;

suppose i in {.(n + 1).} ; :: thesis: ((Binary z) ^ <*(IFEQ d,FALSE ,0 ,(2 to_power n))*>) /. i = IFEQ ((z ^ <*d*>) /. i),FALSE ,0 ,(2 to_power (i -' 1))

then A4: i = n + 1 by TARSKI:def 1;
hence ((Binary z) ^ <*(IFEQ d,FALSE ,0 ,(2 to_power n))*>) /. i = IFEQ d,FALSE ,0 ,(2 to_power n) by Th3
.= IFEQ ((z ^ <*d*>) /. i),FALSE ,0 ,(2 to_power n) by A4, Th3
.= IFEQ ((z ^ <*d*>) /. i),FALSE ,0 ,(2 to_power (i -' 1)) by A4, NAT_D:34 ;
:: thesis: verum

end;

end;

end;

hence Absval (z ^ <*d*>) = addnat $$ ((Binary z) ^ <*(IFEQ d,FALSE ,0 ,(2 to_power n))*>) by Def6
.= addnat . (addnat $$ (Binary z)),(IFEQ d,FALSE ,0 ,(2 to_power n)) by FINSOP_1:5
.= (Absval z) + (IFEQ d,FALSE ,0 ,(2 to_power n)) by BINOP_2:def 23 ;
:: thesis: verum