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:25;
1 in Seg 1 ;
then A3: (Binary z1) /. 1 = IFEQ (z1 /. 1),FALSE ,0 ,(2 to_power (1 -' 1)) by Def6
.= 2 to_power (1 -' 1) by A2, FUNCOP_1:def 8 ;
ex k being Element of NAT st Binary z1 = <*k*> by FINSEQ_2:117;
hence Absval z1 = addnat $$ <*(2 to_power (1 -' 1))*> by A3, FINSEQ_4:25
.= 2 to_power (1 -' 1) by FINSOP_1:12
.= 2 to_power 0 by A1, XREAL_0:def 2
.= 1 by POWER:29 ;
:: thesis: verum