let A be set ; :: thesis: for C being non empty set
for B being Subset of A
for f, g being Function of A,C holds (g | B) +* f = f
let C be non empty set ; :: thesis: for B being Subset of A
for f, g being Function of A,C holds (g | B) +* f = f
let B be Subset of A; :: thesis: for f, g being Function of A,C holds (g | B) +* f = f
let f, g be Function of A,C; :: thesis: (g | B) +* f = f
( dom (g | B) = B & dom f = A ) by Th1, FUNCT_2:def 1;
hence (g | B) +* f = f by FUNCT_4:19; :: thesis: verum