let x, y be object ; :: thesis: for p being DTree-yielding FinSequence holds

( 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 ) ) )

let p be DTree-yielding FinSequence; :: thesis: ( 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 ) ) )

A1: dom (x -tree p) = tree (doms p) by Th10;

( i < len p & T = p . (i + 1) & y = <*i*> ^ q ) ) ) by A1, A2, TREES_3:def 15; :: thesis: verum

( 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 ) ) )

let p be DTree-yielding FinSequence; :: thesis: ( 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 ) ) )

A1: dom (x -tree p) = tree (doms p) by Th10;

A2: now :: thesis: ( ex i being Nat ex q being FinSequence st

( i < len (doms p) & q in (doms p) . (i + 1) & y = <*i*> ^ q ) implies 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 ) )

( i < len (doms p) & q in (doms p) . (i + 1) & y = <*i*> ^ q ) implies 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 ) )

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: 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 )

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: 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, A6, FUNCT_6:22;

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:38; :: thesis: verum

end;A4: q in (doms p) . (i + 1) and

A5: y = <*i*> ^ q ; :: thesis: 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 )

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: 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, A6, FUNCT_6:22;

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:38; :: thesis: verum

now :: thesis: ( 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 ) implies ex i being Nat ex q being FinSequence st

( i < len (doms p) & q in (doms p) . (i + 1) & y = <*i*> ^ q ) )

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 ) implies ex i being Nat ex q being FinSequence st

( i < len (doms p) & q in (doms p) . (i + 1) & y = <*i*> ^ q ) )

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: ex i being 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 )

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: verum

end;A8: T = p . (i + 1) and

A9: y = <*i*> ^ q ; :: thesis: ex i being 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 )

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: verum

( i < len p & T = p . (i + 1) & y = <*i*> ^ q ) ) ) by A1, A2, TREES_3:def 15; :: thesis: verum