let f be FinSequence; :: thesis: ( f is empty implies f is 0 -long )
assume f is empty ; :: thesis: f is 0 -long
then len f = 0 ;
hence f is 0 -long by Def18; :: thesis: verum