:: deftheorem Def7 defines <- TREES_4:def 7 :
for T, T9 being DecoratedTree
for x being set
for b₄ being DecoratedTree holds
( b₄ = (T,x) <- T9 iff ( ( for p being FinSequence holds
( p in dom b₄ iff ( p in dom T or ex q being Node of T ex r being Node of T9 st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
b₄ . p = T . p ) & ( for p being Node of T
for q being Node of T9 st p in Leaves (dom T) & T . p = x holds
b₄ . (p ^ q) = T9 . q ) ) );