f </> g = f <#> (g ") ;
hence f </> g is PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y)) by VALUED_1:def 7; :: thesis: verum