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