reconsider g = T as Function of (dom T),D by Lm2;
reconsider fg = f * g as Function of (dom T),E ;
rng fg c= E ;
hence f * T is DecoratedTree-like ; :: thesis: verum