reconsider f = idseq n as n -element FinSequence ;
let g be FinSequence; :: thesis: ( g is n -element implies g is Seg n -defined )
assume g is n -element ; :: thesis: g is Seg n -defined
then len g = len f by FINSEQ_3:153;
then dom g = dom (id (Seg n)) by FINSEQ_3:29;
hence g is Seg n -defined by RELAT_1:def 18; :: thesis: verum