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

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