thus ex f being Function of (TS PeanoNat),NAT st
( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
f . (root-tree t) = H₁(t) ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
f . (nt -tree ts) = H₃(nt, roots ts,f * ts) ) ) from DTCONSTR:sch 8(); :: thesis: verum