reconsider g = T as Function of dom T,D by Lm3;
reconsider fg = f * g as Function of dom T,E ;
rng fg c= E ;
hence T * f is DecoratedTree of E by TREES_2:def 9; :: thesis: verum