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