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 that
A1: root-tree x = y -tree p and
A2: p is DTree-yielding ; :: thesis: ( x = y & p = {} )
reconsider p9 = p as DTree-yielding FinSequence by A2;
thus x = (root-tree x) . {} by Th3
.= y by A1, A2, Def4 ; :: thesis: p = {}
A3: dom (y -tree p) = tree (doms p9) by Th10;
A4: doms p = {} by A1, A3, Th3, TREES_3:53, TREES_3:55;
A5: dom (doms p) = dom p by A3, TREES_3:39;
thus p = {} by A4, A5; :: thesis: verum