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