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:117;
assume
z1 = <*FALSE *>
; Absval z1 = 0
then A2:
z1 /. 1 = FALSE
by FINSEQ_4:25;
1 in Seg 1
;
then (Binary z1) /. 1 =
IFEQ (z1 /. 1),FALSE ,0 ,(2 to_power (1 -' 1))
by Def6
.=
0
by A2, FUNCOP_1:def 8
;
hence Absval z1 =
addnat $$ <*0 *>
by A1, FINSEQ_4:25
.=
0
by FINSOP_1:12
;
verum