<*x*> is FinSequence of PFuncs ((A *),A) ;
hence <*x*> is PFuncFinSequence of A ; :: thesis: verum