theorem Th9: :: PDLAX:9

for f being PartFunc of REAL,REAL holds f + f = 2 (#) f