dom (f1 | ((dom f1) \ (dom f2))) = (dom f1) \ (dom f2) by RELAT_1:62;
hence f2 \/ (f1 | ((dom f1) \ (dom f2))) is Function-like by GRFUNC_1:13, XBOOLE_1:79; :: thesis: verum