:: deftheorem Def10 defines | TREES_2:def 10 :
for T being DecoratedTree
for p being FinSequence of NAT
for b₃ being DecoratedTree holds
( b₃ = T | p iff ( dom b₃ = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
b₃ . q = T . (p ^ q) ) ) );