let x, y be set ; :: thesis: for p being FinSequence st root-tree x = y -tree p & p is DTree-yielding holds
( x = y & p = {} )
let p be FinSequence; :: thesis: ( root-tree x = y -tree p & p is DTree-yielding implies ( x = y & p = {} ) )
assume A1: ( root-tree x = y -tree p & p is DTree-yielding ) ; :: thesis: ( x = y & p = {} )
then reconsider p' = p as DTree-yielding FinSequence ;
thus x = (root-tree x) . {} by Th3
.= y by A1, Def4 ; :: thesis: p = {}
( dom (y -tree p) = tree (doms p') & dom (root-tree x) = elementary_tree 0 ) by Th3, Th10;
then ( doms p = {} & dom (doms p) = dom p & dom {} = {} ) by A1, TREES_3:39, TREES_3:53, TREES_3:55;
hence p = {} ; :: thesis: verum