let A be set ; :: thesis: for C being non empty set
for g being Function of A,C
for B being Finite_Subset of A holds dom (g | B) = B
let C be non empty set ; :: thesis: for g being Function of A,C
for B being Finite_Subset of A holds dom (g | B) = B
let g be Function of A,C; :: thesis: for B being Finite_Subset of A holds dom (g | B) = B
let B be Finite_Subset of A; :: thesis: dom (g | B) = B
reconsider C = B as Subset of A by FINSUB_1:17;
dom (g | C) = C by Th2;
hence dom (g | B) = B ; :: thesis: verum