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