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