let z1 be Tuple of 1,BOOLEAN ; :: thesis: ( z1 = <*TRUE *> implies Absval z1 = 1 )
assume A1: z1 = <*TRUE *> ; :: thesis: Absval z1 = 1
consider k being Element of NAT such that
A2: Binary z1 = <*k*> by FINSEQ_2:117;
A3: z1 /. 1 <> FALSE by A1, FINSEQ_4:25;
1 in Seg 1 ;
then A4: (Binary z1) /. 1 = IFEQ (z1 /. 1),FALSE ,0 ,(2 to_power (1 -' 1)) by Def6
.= 2 to_power (1 -' 1) by A3, FUNCOP_1:def 8 ;
A5: 1 - 1 = 0 ;
thus Absval z1 = addnat $$ <*(2 to_power (1 -' 1))*> by A2, A4, FINSEQ_4:25
.= 2 to_power (1 -' 1) by FINSOP_1:12
.= 2 to_power 0 by A5, XREAL_0:def 2
.= 1 by POWER:29 ; :: thesis: verum