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 = (x -flat_tree p) . {} 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 0)) = elementary_tree (len p) by TREES_3:54

.= dom (x -flat_tree p) by Def3

.= tree (doms q9) by A1, Th10 ;

then A3: (len p) |-> (elementary_tree 0) = doms q9 by TREES_3:50;

len (doms q9) = len q by TREES_3:38;

hence A4: len p = len q by A3, CARD_1:def 7; :: 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 A5, FINSEQ_3:25;

consider n being Nat such that

A8: i = 1 + n by A6, NAT_1:10;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

A9: n < len p by A7, A8, NAT_1:13;

then (x -flat_tree p) | <*n*> = root-tree (p . i) by A8, Th9;

hence q . i = root-tree (p . i) by A1, A2, A4, A8, A9, Def4; :: thesis: verum

( 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 = (x -flat_tree p) . {} 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 0)) = elementary_tree (len p) by TREES_3:54

.= dom (x -flat_tree p) by Def3

.= tree (doms q9) by A1, Th10 ;

then A3: (len p) |-> (elementary_tree 0) = doms q9 by TREES_3:50;

len (doms q9) = len q by TREES_3:38;

hence A4: len p = len q by A3, CARD_1:def 7; :: 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 A5, FINSEQ_3:25;

consider n being Nat such that

A8: i = 1 + n by A6, NAT_1:10;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

A9: n < len p by A7, A8, NAT_1:13;

then (x -flat_tree p) | <*n*> = root-tree (p . i) by A8, Th9;

hence q . i = root-tree (p . i) by A1, A2, A4, A8, A9, Def4; :: thesis: verum