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