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

( 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