( dom (doms p) = dom p & Seg (len p) = dom p ) by Th39, FINSEQ_1:def 3;
hence ( doms p is Tree-yielding & doms p is FinSequence-like ) by Th39, FINSEQ_1:def 2; :: thesis: verum