scheme :: TREES_9:sch 2
ExDecTrees{ F1() -> non empty set , F2() -> Element of F1(), F3( object ) -> FinSequence of F1() } :
ex T being finite-branching DecoratedTree of F1() st
( T . {} = F2() & ( for t being Element of dom T
for w being Element of F1() st w = T . t holds
succ (T,t) = F3(w) ) )