let z1 be Tuple of 1, BOOLEAN ; :: thesis: ( z1 = <*TRUE*> implies Absval z1 = 1 )
A1: 1 - 1 = 0 ;
assume z1 = <*TRUE*> ; :: thesis: Absval z1 = 1
then A2: z1 /. 1 <> FALSE by FINSEQ_4:16;
1 in Seg 1 ;
then A3: (Binary z1) /. 1 = IFEQ ((z1 /. 1),FALSE,0,(2 to_power (1 -' 1))) by Def3
.= 2 to_power (1 -' 1) by A2, FUNCOP_1:def 8 ;
ex k being Element of NAT st Binary z1 = <*k*> by FINSEQ_2:97;
hence Absval z1 = addnat $$ <*(2 to_power (1 -' 1))*> by A3, FINSEQ_4:16
.= 2 to_power (1 -' 1) by FINSOP_1:11
.= 2 to_power 0 by A1, XREAL_0:def 2
.= 1 by POWER:24 ;
:: thesis: verum