( dom (pr2 f) = dom f & dom f = Seg (len f) ) by MCART_1:def 13, FINSEQ_1:def 3;
hence pr2 f is FinSequence-like by FINSEQ_1:def 2; :: thesis: verum