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 ; :: thesis: verum