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