let f be FinSequence; :: thesis: ( f is total & f is Seg n -defined implies f is n -element )
assume ( f is total & f is Seg n -defined ) ; :: thesis: f is n -element
then Seg n = dom f by PARTFUN1:def 2;
then Seg (len f) = Seg n by FINSEQ_1:def 3;
hence f is n -element by CARD_1:def 7, FINSEQ_1:6; :: thesis: verum