let x, y be object ; :: 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 = {}
dom (y -tree p) = tree (doms p9) by Th10;
then A3: doms p9 = {} by A1, TREES_3:50, TREES_3:52;
dom (doms p9) = dom p by TREES_3:37;
hence p = {} by A3; :: thesis: verum