let X be set ; :: thesis: for f being Function st X c= f holds
dom (f \ X) = (dom f) \ (proj1 X)
let f be Function; :: thesis: ( X c= f implies dom (f \ X) = (dom f) \ (proj1 X) )
assume X c= f ; :: thesis: dom (f \ X) = (dom f) \ (proj1 X)
then reconsider g = X as Relation-like Function-like Subset of f ;
set dg = dom g;
set df = dom f;
f | (dom g) = g by GRFUNC_1:23;
hence dom (f \ X) = (dom f) \ (proj1 X) by RELAT_1:177; :: thesis: verum