let h be Subset of g; :: thesis: h is f -compatible
h = g | (dom h) by Th96;
hence h is f -compatible ; :: thesis: verum