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