reconsider f = f, g = g as Element of PFuncs (A,B) ;
F . (f,g) is Element of PFuncs (A,B) ;
hence F . (f,g) is Element of PFuncs (A,B) ; :: thesis: verum