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