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:9;
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 Th1
.= IFEQ ((z /. i),FALSE,0,(2 to_power (i -' 1))) by A3, Def3
.= IFEQ (((z ^ <*d*>) /. i),FALSE,0,(2 to_power (i -' 1))) by A3, Th1 ;
:: 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 Th2
.= IFEQ (((z ^ <*d*>) /. i),FALSE,0,(2 to_power n)) by A4, Th2
.= 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 Def3
.= addnat . ((addnat $$ (Binary z)),(IFEQ (d,FALSE,0,(2 to_power n)))) by FINSOP_1:4
.= (Absval z) + (IFEQ (d,FALSE,0,(2 to_power n))) by BINOP_2:def 23 ;
:: thesis: verum