:: deftheorem Def14 defines pi FREEALG:def 14 :
for f being non empty FinSequence of NAT
for D being non empty disjoint_with_NAT set
for C being non empty set
for s being Symbol of (DTConUA (f,D))
for F being Function of (FreeGenSetNSG (f,D)),C st s in Terminals (DTConUA (f,D)) holds
pi (F,s) = F . (root-tree s);