let g be FinSequence; :: thesis: ( g is len f -element implies g is dom f -defined )
assume g is len f -element ; :: thesis: g is dom f -defined
then len f = len g by CARD_1:def 7;
then dom f = dom g by FINSEQ_3:29;
hence g is dom f -defined by RELAT_1:def 18; :: thesis: verum