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