theorem Th7: :: GROUP_20:7

for f being Function
for i, x being set holds f = (f +* (i,x)) +* (i,(f . i))