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