ex X1 being Subset of (FinTrees the carrier of F₂()) st
( X1 = { (t `1) where t is Element of FinTrees [: the carrier of F₂(),F₃():] : t in Union F₁() } & ( for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree d in X1 ) & ( for o being Symbol of F₂()
for p being FinSequence of X1 st o ==> roots p holds
o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F₂()) st ( for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree d in F ) & ( for o being Symbol of F₂()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
X1 c= F ) )

A1: dom F₁() = NAT and
A2: F₁() . 0 = { (root-tree [t,d]) where t is Symbol of F₂(), d is Element of F₃() : ( ( t in Terminals F₂() & d = F₄(t) ) or ( t ==> {} & d = F₅(t,{},{}) ) ) } and
A3: for n being Nat holds F₁() . (n + 1) = (F₁() . n) \/ { ([o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F₂(), p is Element of (F₁() . n) * : ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( p = q & o ==> pr1 (roots q) ) }