theorem Th114: :: FUNCT_7:115

for A, B, a, b being set
for f being Function of A,B st b in B holds
f +* (a,b) is Function of A,B