f [/] c = f [#] (c " ) ;
hence f [/] c is PartFunc of X,(Q_PFuncs (DOMS Y)) ; :: thesis: verum