theorem Th3: :: LATTICE2:3

for A being set
for C being non empty set
for f, g being Function of A,C
for B being set holds f +* (g | B) is Function of A,C