let f be FinSeqLen of 0 ; :: thesis: f is empty
len f = 0 by Def12;
hence f is empty ; :: thesis: verum