given i being 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:
len (doms p) = len p by TREES_3:38;
then A6: i + 1 in dom p by A3, Lm2;
then reconsider T = p . (i + 1) as DecoratedTree by TREES_3:24;
take i = i; :: thesis:
take T = T; :: thesis:
reconsider q = q as Node of T by A4, A6, FUNCT_6:22;
take q = q; :: thesis:
thus ( i < len p & T = p . (i + 1) & y = <*i*> ^ q ) by A3, A5, TREES_3:38; :: thesis:

end;

given i being Nat, T being DecoratedTree, q being Node of T such that A7: i < len p and
A8: T = p . (i + 1) and
A9: y = <*i*> ^ q ; :: thesis:
reconsider q = q as FinSequence ;
take i = i; :: thesis:
take q = q; :: thesis:
i + 1 in dom p by A7, Lm2;
then (doms p) . (i + 1) = dom T by A8, FUNCT_6:22;
hence ( i < len (doms p) & q in (doms p) . (i + 1) & y = <*i*> ^ q ) by A7, A9, TREES_3:38; :: thesis:

end;

hence ( y in dom (x -tree p) iff ( y = {} or ex i being 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, TREES_3:def 15; :: thesis: