theorem Th5: :: MODAL_1:10

for t1 being DecoratedTree of [:NAT,NAT:] holds t1 in PFuncs ((NAT *),[:NAT,NAT:])