theorem Th102: :: FUNCT_4:102

for f being Function
for x being object holds f +~ (x,x) = f