deffunc H₁( FinSequence) -> set = T . (p ^ $1);
thus ex t being DecoratedTree st
( dom t = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
t . q = H₁(q) ) ) from TREES_2:sch 7(); :: thesis: verum