theorem :: LATTICE2:6

for A being set
for C being non empty set
for B being Subset of A
for f being Function of A,C holds f +* (f | B) = f by Th5, RELAT_1:59;