let x be Element of BOOLEAN * ; :: thesis: ( len x = 0 implies ExAbsval x = 0 )
consider n being Nat, y being Tuple of n, BOOLEAN such that
y: ( y = x & ExAbsval x = Absval y ) by Def100;
assume len x = 0 ; :: thesis: ExAbsval x = 0
then n = 0 by y;
then lb: len (Binary y) = 0 ;
thus ExAbsval x = Absval y by y
.= addnat $$ (Binary y) by BINARITH:def 4
.= the_unity_wrt addnat by lb, FINSOP_1:def 1
.= 0 by BINOP_2:5 ; :: thesis: verum