theorem Th115: :: FUNCT_7:116

for A being set
for f being Function
for x, y being object st rng f c= A holds
f +~ (x,y) = ((id A) +* (x,y)) * f