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