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