scheme :: TREES_2:sch 9
DTreeStructFinEx{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( set ) -> Nat, F₄() -> Function of [:F₁(),NAT:],F₁() } :

ex T being DecoratedTree of F₁() st
( T . {} = F₂() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k < F₃((T . t)) } & ( for n being Nat st n < F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . ((T . t),n) ) ) ) )