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