let t1 be DecoratedTree of [:NAT,NAT:]; :: thesis: t1 in PFuncs ((NAT *),[:NAT,NAT:])
( rng t1 c= [:NAT,NAT:] & dom t1 c= NAT * ) by TREES_1:def 3;
hence t1 in PFuncs ((NAT *),[:NAT,NAT:]) by PARTFUN1:def 3; :: thesis: verum