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 A1: ( x -flat_tree p = y -tree q & 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) ) )
then reconsider q' = q as DTree-yielding FinSequence ;
thus x = (x -flat_tree p) . {} by Def3
.= y by A1, 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 q') by A1, Th10 ;
then ( (len p) |-> (elementary_tree 0 ) = doms q' & len (doms q') = len q ) by TREES_3:40, TREES_3:53;
hence A2: len p = len q by 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 i in dom p ; :: thesis: q . i = root-tree (p . i)
then A3: ( i >= 1 & i <= len p ) by FINSEQ_3:27;
then consider n being Nat such that
A4: i = 1 + n by NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
n < len p by A3, A4, NAT_1:13;
then ( (x -flat_tree p) | <*n*> = root-tree (p . i) & (y -tree q) | <*n*> = q . i ) by A1, A2, A4, Def4, Th9;
hence q . i = root-tree (p . i) by A1; :: thesis: verum