let x, y be set ; :: 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 Element of 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 Element of 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 Element of 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 Element of 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:57
.= dom (x -flat_tree p) by Def3
.= tree (doms q9) by A1, Th10 ;
then A4: (len p) |-> (elementary_tree 0 ) = doms q9 by TREES_3:53;
len (doms q9) = len q by TREES_3:40;
hence A6: len p = len q by A4, FINSEQ_1:def 18; :: thesis: for i being Element of NAT st i in dom p holds
q . i = root-tree (p . i)
let i be Element of NAT ; :: thesis: ( i in dom p implies q . i = root-tree (p . i) )
assume A7: i in dom p ; :: thesis: q . i = root-tree (p . i)
then A8: i >= 1 by FINSEQ_3:27;
A9: i <= len p by A7, FINSEQ_3:27;
consider n being Nat such that
A10: i = 1 + n by A8, NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A11: n < len p by A9, A10, NAT_1:13;
then (x -flat_tree p) | <*n*> = root-tree (p . i) by A10, Th9;
hence q . i = root-tree (p . i) by A1, A2, A6, A10, A11, Def4; :: thesis: verum