let p be DTree-yielding FinSequence; :: thesis: len (doms p) = len p
A1: dom p = dom (doms p) by Th37;
Seg (len p) = dom p by FINSEQ_1:def 3;
hence len (doms p) = len p by A1, FINSEQ_1:def 3; :: thesis: verum