let x, y be object ; :: thesis: for p, q being FinSequence st x -flat_tree p = y -tree q & q is DTree-yielding holds
( x = y & len p = len q & ( for i being Nat st i in dom p holds
q . i = root-tree (p . i) ) )

let p, q be FinSequence; :: thesis: ( x -flat_tree p = y -tree q & q is DTree-yielding implies ( x = y & len p = len q & ( for i being Nat st i in dom p holds
q . i = root-tree (p . i) ) ) )

assume that
A1: x -flat_tree p = y -tree q and
A2: q is DTree-yielding ; :: thesis: ( x = y & len p = len q & ( for i being Nat st i in dom p holds
q . i = root-tree (p . i) ) )

reconsider q9 = q as DTree-yielding FinSequence by A2;
thus x = () . {} by Def3
.= y by A1, A2, Def4 ; :: thesis: ( len p = len q & ( for i being Nat st i in dom p holds
q . i = root-tree (p . i) ) )

tree ((len p) |-> ) = elementary_tree (len p) by TREES_3:54
.= dom () by Def3
.= tree (doms q9) by ;
then A3: (len p) |-> = doms q9 by TREES_3:50;
len (doms q9) = len q by TREES_3:38;
hence A4: len p = len q by ; :: thesis: for i being Nat st i in dom p holds
q . i = root-tree (p . i)

let i be Nat; :: thesis: ( i in dom p implies q . i = root-tree (p . i) )
assume A5: i in dom p ; :: thesis: q . i = root-tree (p . i)
then A6: i >= 1 by FINSEQ_3:25;
A7: i <= len p by ;
consider n being Nat such that
A8: i = 1 + n by ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A9: n < len p by ;
then (x -flat_tree p) | <*n*> = root-tree (p . i) by ;
hence q . i = root-tree (p . i) by A1, A2, A4, A8, A9, Def4; :: thesis: verum