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