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