let x be object ; :: thesis: for p being DTree-yielding FinSequence holds dom (x -tree p) = tree (doms p)
let p be DTree-yielding FinSequence; :: thesis: dom (x -tree p) = tree (doms p)
ex q being DTree-yielding FinSequence st
( p = q & dom (x -tree p) = tree (doms q) ) by Def4;
hence dom (x -tree p) = tree (doms p) ; :: thesis: verum