let f be FinSequence; :: thesis: not 0 in dom f
assume 0 in dom f ; :: thesis: contradiction
then 0 in Seg (len f) by FINSEQ_1:def 3;
hence contradiction by FINSEQ_1:1; :: thesis: verum