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