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