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