let y, x be set ; :: thesis: for p being DTree-yielding FinSequence holds
( y in dom (x -tree p) iff ( y = {} or ex i being Element of NAT ex T being DecoratedTree ex q being Node of T st
( i < len p & T = p . (i + 1) & y = <*i*> ^ q ) ) )
let p be DTree-yielding FinSequence; :: thesis: ( y in dom (x -tree p) iff ( y = {} or ex i being Element of NAT ex T being DecoratedTree ex q being Node of T st
( i < len p & T = p . (i + 1) & y = <*i*> ^ q ) ) )
A1: dom (x -tree p) = tree (doms p) by Th10;

A2: now

given i being Element of NAT , q being FinSequence such that A3: i < len (doms p) and
A4: q in (doms p) . (i + 1) and
A5: y = <*i*> ^ q ; :: thesis: ex i being Element of NAT ex T being DecoratedTree ex q being Node of T st
( i < len p & T = p . (i + 1) & y = <*i*> ^ q )
A6: len (doms p) = len p by TREES_3:40;
A7: i + 1 in dom p by A3, A6, Lm2;
reconsider T = p . (i + 1) as DecoratedTree by A7, TREES_3:26;
take i = i; :: thesis: ex T being DecoratedTree ex q being Node of T st
( i < len p & T = p . (i + 1) & y = <*i*> ^ q )
take T = T; :: thesis: ex q being Node of T st
( i < len p & T = p . (i + 1) & y = <*i*> ^ q )
reconsider q = q as Node of T by A4, A7, FUNCT_6:31;
take q = q; :: thesis: ( i < len p & T = p . (i + 1) & y = <*i*> ^ q )
thus ( i < len p & T = p . (i + 1) & y = <*i*> ^ q ) by A3, A5, TREES_3:40; :: thesis: verum

end;

A8: now

given i being Element of NAT , T being DecoratedTree, q being Node of T such that A9: i < len p and
A10: T = p . (i + 1) and
A11: y = <*i*> ^ q ; :: thesis: ex i being Element of NAT ex q being FinSequence st
( i < len (doms p) & q in (doms p) . (i + 1) & y = <*i*> ^ q )
reconsider q = q as FinSequence ;
take i = i; :: thesis: ex q being FinSequence st
( i < len (doms p) & q in (doms p) . (i + 1) & y = <*i*> ^ q )
take q = q; :: thesis: ( i < len (doms p) & q in (doms p) . (i + 1) & y = <*i*> ^ q )
A12: i + 1 in dom p by A9, Lm2;
A13: (doms p) . (i + 1) = dom T by A10, A12, FUNCT_6:31;
thus ( i < len (doms p) & q in (doms p) . (i + 1) & y = <*i*> ^ q ) by A9, A11, A13, TREES_3:40; :: thesis: verum

end;

thus ( y in dom (x -tree p) iff ( y = {} or ex i being Element of NAT ex T being DecoratedTree ex q being Node of T st
( i < len p & T = p . (i + 1) & y = <*i*> ^ q ) ) ) by A1, A2, A8, TREES_3:def 15; :: thesis: verum