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