theorem Th7: :: LATTICE2:7

for A being set
for C being non empty set
for B being Subset of A
for f, g being Function of A,C st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f